Does a System to Automatically (Mathematically) Generate Arbitrary Computer Programs Really Exist? 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.
Prolog, being just a programming language, does not avoid the problem of having to write a computer program.  You are just writing it in one language and translating that into another programming language.

What is needed is to input a formula of logic that is true iff the output satisfies the desired conditions.  For example, (exists A)A*I=J means I is a factor of J and is a valid specification for a program to follow.  It means to input I and J, and output TRUE or FALSE depending on whether or not I is a factor of J or not.

Have anybody developed a system to take a formula of logic and create computer programs that meet its requirement?  Professors say yes but none has even been published.