Has anyone actually developed a Program Synthesis system for creating computer programs automatically from a non-procedural specification that is taken from a fairly robust system of specifications? For example, I might say "Check if X is a factor of Y." or "List all prime numbers between X and Y." and out pops a program or two written in PHP that does just that.
I would actually pay money for an example that shows that the answer is yes.
Let's say you have relations for less than and multiplication, and you give a wff of logic. So it can be (exists A)MUL(A,X,Y) where MUL(A,B,C) iff A x B = C, for the first specification above. For the second specification with output of a number (the prime numbers) instead of TRUE or FALSE, we could say variable N means output all values of N such that the wff is TRUE.
I have heard the claim that the answer is yes, but articles give no real examples of its being used. Either there is no example, or what they call an example merely displays a program and claims that it was or can be generated by some system that is imagined or even described in detail, but the example lacks any details at all.
Can someone give a complete example of a system, a specification, the resulting program(s) and step-by-step exactly how that program is automatically constructed?
And if an example is given, could it be a simple program with only a few steps to create, rather than dozens of pages of formulas that would take months to go through and is suspect of being obfuscation hiding the fact that it is not genuine?
Depending on what exactly "non-procedural specification" means, prolog might match your requirements.
Prolog is a so-called declarative programming language where you don't specify that steps that an algorithm perform, but rather describe it's result in (a version of) first-order logic. There are compilers for prolog, which translate this declarative description into a procedural one.