11 ms·

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 Pro

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?

Tainnor 1y ago
This is impossible to solve in the general case due to Gödel's first incompleteness theorem.
- YeGoblynQueenne 1y ago
  A compiler is a program synthesizer that takes in a specification in a high-level language and produces an equivalent program in machine code. Given that observation, can you explain what you mean that this is impossible to solve?
  - Tainnor 1y ago
    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). 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.
    - YeGoblynQueenne 1y ago
      I'm sorry but I think that when I replied to your comment it didn't have the "in the general case". I might have missed that, but I thought you meant it's impossible to do it at all. 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.
      - Tainnor 1y ago
        I didn't edit my original comment. Compilers are totally besides the point. Python, Java and even Prolog aren't FOL, they lack its expressive power.
        YeGoblynQueenne 1y ago
        Then I misunderstood your comment, but at the same time your comment is correct but irrelevant to the OP. "In the general case" there are undecidable problems, and there may even be an infinite number of undecidable problems, but there are most likely an infinite number of decidable problems also. 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: https://en.wikipedia.org/wiki/Z_notation https://en.wikipedia.org/wiki/Z_notation
  - Gajurgensen 1y ago
    Think of higher level specifications which do not imply any details of the implementation. 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."
    - YeGoblynQueenne 1y ago
      >> Think of higher level specifications which do not imply any details of the implementation. 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.
emorning3 1y ago
PS... 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.
Gajurgensen 1y ago
Program synthesis is of course very difficult in general, especially if you want it to be entirely automated. One option to make it more practical is to have the user drive synthesis from specification to implementation via something which looks like a sequence of tactics. (I'll add a plug to some stuff we are working on at Kestrel: https://www.cs.utexas.edu/~moore/acl2/manuals/latest/index.html?topic=APT____APT 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.

Tainnor 1y ago

This is impossible to solve in the general case due to Gödel's first incompleteness theorem.

YeGoblynQueenne 1y ago
A compiler is a program synthesizer that takes in a specification in a high-level language and produces an equivalent program in machine code. Given that observation, can you explain what you mean that this is impossible to solve?
- Tainnor 1y ago
  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). 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.
  - YeGoblynQueenne 1y ago
    I'm sorry but I think that when I replied to your comment it didn't have the "in the general case". I might have missed that, but I thought you meant it's impossible to do it at all. 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.
    - Tainnor 1y ago
      I didn't edit my original comment. Compilers are totally besides the point. Python, Java and even Prolog aren't FOL, they lack its expressive power.
      - YeGoblynQueenne 1y ago
        Then I misunderstood your comment, but at the same time your comment is correct but irrelevant to the OP. "In the general case" there are undecidable problems, and there may even be an infinite number of undecidable problems, but there are most likely an infinite number of decidable problems also. 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: https://en.wikipedia.org/wiki/Z_notation https://en.wikipedia.org/wiki/Z_notation
- Gajurgensen 1y ago
  Think of higher level specifications which do not imply any details of the implementation. 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."
  - YeGoblynQueenne 1y ago
    >> Think of higher level specifications which do not imply any details of the implementation. 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.

emorning3 1y ago

PS... 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.

Gajurgensen 1y ago

Program synthesis is of course very difficult in general, especially if you want it to be entirely automated. One option to make it more practical is to have the user drive synthesis from specification to implementation via something which looks like a sequence of tactics. (I'll add a plug to some stuff we are working on at Kestrel: https://www.cs.utexas.edu/~moore/acl2/manuals/latest/index.html?topic=APT____APT 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.