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.
>>Another way to see it is that the set of valid theorems in FOL is uncomputable.<<
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.
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.
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:
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."
>> 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.
Given that observation, can you explain what you mean that this is impossible to solve?