Hacker News new | ask | show | jobs
by bjornjajayaja 1832 days ago
I’d love to see a language where you write the tests and then the compiler creates the application code.
10 comments

This is an active field of research. Search for "program synthesis".

We are advancing, but the current state is... not mind-blowing yet (albeit somewhat cool!). See [1] for an example interactive demo and [2] for the corresponding presentation.

[1] http://comcom.csail.mit.edu/comcom/#Synquid

[2] https://www.youtube.com/watch?v=HnOix9TFy1A

I was in the audience for that talk. The recording doesn't capture how much energy there was- we were all gasping and cheering throughout.

Still a decade off from production, though. That it doesn't just take "test cases": you have to know how to formally express the program properties, which is a separate skill from both unit testing and implementing.

Is this not almost how logic programming (prolog, etc.) works? You tell the language some things which are true, and then it'll be able to infer answers to "questions" you ask:

https://wiki.c2.com/?LogicProgramming

Let's say we work on the "reverse list" function. A few tests I could write are that the following clauses are true:

    rev([1], [1])
    rev([1, 2, 3], [3, 2, 1])
And maybe also that the following clauses are false:

    rev([1, 2], [1, 2])
    rev([], [1])
    rev([1, 1], [1])
Is Prolog able to infer, from the above, that rev([4, 5], [5, 4]) ? Or to synthesize the general form rev([H|T],R) :- rev(T, RT), concat(RT,[H],R) ?
Sounds like NN training that could be achievable. The problem comes with unit testing, because the minimal testable unit could be more complex than a function.
Yeah. I've often seen TDD where you act both as the logic programmer writing the tests and the imperative programmer writing the implementation.
No. Not even a little bit.
Could... could you enlighten me please?
It's incredibly easy. First, you start with a customer that actually knows exactly what they want.
This sounds a lot lke like minikanren (https://github.com/webyrd/Barliman) where you give test cases and Idris2 (https://github.com/idris-lang/Idris2) where you give type constraints as a tool for building programs.
We typically write _sample_ tests in boolean logic, which isn't quite expressive enough for this.

But if you look at logic programming with more expressive systems you can have something like what you propose. We describe what we expect to have and the system deduces a result. Not quite what you want but its closer.

Now there is also an ubiquitous logic system that many use: static typing. In a sense you are describing the general properties of something and the compiler infers optimizations based on your assertions. The concrete program is not a line by line translation from your code to machine code, but perhaps looked at in its entirety.

I agree that there is a lot of merit in pushing these things further and further. Right now we're kind of in a stage of patching things together. But I hope and assume that programming becomes more holistic in the future. Ironically we have to look at the past first, there was a lot of momentum in this direction up until the 80's roughly.

How would this even work? At best you might get a set of class/function stubs with some minimal logic. At worst what you'd have is a compiler that is actually a complicated, truly AGI brain, which could produce some truly awful code. In which case you've simply reproduced TDD's normal result: truly awful code.

Aside from that, to produce a program that did what is actually required would require test cases and functions that cover the set of inputs and outputs. This is trivial for mathematical functions, but impractical (or impossible) for more general applications (e.g. anything dealing with human inputs).

You could just use a fuzzer to generate code, and run tests on the output. Each new test would approximately double the run time until a new "correct" output was found.

This doesn't become practical until you can do it on a quantum computer with millions of cubits.

This is kinda what logic programming is, like in prolog. You tell the computer what you want, and it finds the answer for you.

TDD is where you both write what you want, and you do the implementation also.

I would like to see this language handle some lawmaker-specified code.

Show examples of French retirement pension computation, and watch if a computer can actually commit petit-suicide.

Well, that's how machine learning works.
Machine learning requires a problem that you can have partially correct, so that it can climb the gradient to optimize on. If you can build tests that have an analog instead of pass/fail output, you could, in theory, do it with machine learning.

Beware that machine learning in a single pass/fail is more like having an infinite number of monkeys trying to write the works of Isaac Asimov.

[Edit/Update] All of the tests could be individual values, so non-zero (but nowhere near all ones) might help. Thanks for making me reconsider this, sdenton4.

Not all ml is gradient based. Other options exist: Bayesian black box optimization (like vizier), or genetic algos. And Vizier is actually quite efficient for small problems.
With genetic algorithms you still need to be able to calculate a fitness. Usually a test is fail/success. There's no fitness in that. I would guess the other optimizers also need such a signal?
Success/failure is just a binary classification signal: you can look at how it correlates with your target variables, how noisy it is for particular choices of variables over multiple trials, etc. The noisier it is, the harder it is to learn, but such is life.
I think it would be impractical for a naive fitness function that is 0 for failure and 1 for success. Wouldn't the signal be too difficult to find? GA would be brute force until you find code that passed a test. I don't think tests for factorio are trivial.

Maybe you could move the goal/fitness function along the way. So start with something that compiles. Then having the desired input output. Etc.

I was actually thinking about decision trees.