I dont want to prove that my code is correct.
I would prefer to create specifications in logic and have the code derived for me.
Other than something like Prolog, are there tools for working this way?
I would prefer to create specifications in logic and have the code derived for me.
Other than something like Prolog, are there tools for working this way?
(I'll add a plug to some stuff we are working on at Kestrel: https://www.cs.utexas.edu/~moore/acl2/manuals/latest/index.h.... We've used the APT library to do stepwise refinements from specs ACL2 to C code. Each step is something like "make function tail recursive" or "switch to a new, isomorphic shape of the data").
By the way, Curry-Howard offers a compelling insight here: deriving programs from specifications (i.e. types+propositions) may be the same process as deriving proofs from propositions. So the two processes can in principle work the exact same way.
I've been waiting for such tools for 40 years.
I just now realized that vibe coding is probably the closest we'll get in my lifetime.
It's a start I guess.
Given that observation, can you explain what you mean that this is impossible to solve?
If your specification logic is strong enough to enclude basic addition and multiplication (and if it's not, it's probably not very useful), it will be affected by incompleteness. So you can write down the Gödel sentence corresponding to your program synthesiser's inference rule and it won't be able to find either a proof (i.e. an implementation) or a disproof (i.e. failing explicitly), so it will have to loop forever.
Another way to see it is that the set of valid theorems in FOL is uncomputable. To take a concrete example, if you write down the specification for "find the smallest number that is a counterexample to the Goldbach conjecture", finding an implementation for it would be equivalent to answering the conjecture in the negative while getting an error message would mean that the conjecture is true, but obviously nobody has solved it yet.
Btw:
>> OP specifically asked for a program that would derive code from logical specifications, not a run-of-the-mill compiler where you have to write the code yourself (albeit on a higher level).
There's nothing "run-of-the-mill" about compilers and if your high-level language is e.g. FOL, then a compiler that transforms it to low-level machine code is, still, a program synthesizer, and v.v.
Compilers are totally besides the point. Python, Java and even Prolog aren't FOL, they lack its expressive power.
That is to say, undecidability is not like intractability. One can work around undecidability, and one can always find useful problems that can be solved without falling down undecidable holes. So for example, the Halting Problem may be undecidable, but we have computers we use all the time to do a whole bunch of very useful things. FOL is undecidable, but elementary Boolean logic is decidable and definite logic is semi-decidable. Any formal system powerful enough to represent integer arithmetic is undecidable but we use arithmetic, and higher-level maths based on arithmetic, all the time. And so on, and so forth.
The OP is asking for a program synthesiser where they can enter a specification in a logic language and get back a program in some other language. That is perfectly doable in practice, there's an entire field of research that produces work along those lines, the field of Program Synthesis. Modern LLMs can to some extent do that, very unreliably, and of course like I say, a compiler is nothing but a (deductive) program synthesiser, your unwillingness to accept that well-understood truism non-withstanding.
>> Compilers are totally besides the point. Python, Java and even Prolog aren't FOL, they lack its expressive power.
That's incorrect about Prolog. Prolog is SLD-Resolution, i.e. Linear Resolution with a Selection rule restricted to Definite clauses. Definite logic is a restriction of the first order predicate calculus that nevertheless retains its full expressive power, and is semi-decidable (all true statements in definite logic are provable). Most implementations of Prolog executed by Depth-First Search are incomplete because they get stuck in loops, but Prolog executed by SLG-Resolution (a.k.a. tabling) is refutation-complete.
Prolog is probably the closest practical programming language that achieves what the OP is looking for (although not strictly in program synthesis terms) but the OP may also want to check out things like Z notation:
That's exactly the kind of thing I was looking for, thanks!
I've never seen it put that way exactly. And I've never learned the gory details of the incompleteness proofs and I've never made the explicit connection between incompleteness and computation before. That blew my tiny pea brain :-).
Now that I've read the Wikipedia page, I guess I only understood incompleteness as the 2nd theorem.
https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
Thanks!
For instance, consider a sorting function. One could write a bubble sort and consider that a spec, but that is far too much detail, much of which you don't actually care about. A much better specification would be "the function takes a list 'l' and produces a sorted list which is also a permutation of 'l'." This is the sort of specification we want, but we have more work to fill in the implementation details.
This can get arbitrarily difficult if your specification logic is sufficiently expressive. Imagine the spec is something like "solve this unproven mathematical conjecture."
In that case you're talking about inductive program synthesis, i.e. program synthesis from incomplete specifications. Program synthesis from complete specification is what we call deductive program synthesis.
Both are quite possible within the limits of undecidability of sufficiently expressive languages. My question to the OP was why did they think it's not possible at all, but I may have misread their comment.