Has Anyone Actually Created a System that Writes Computer Programs from specification?

Has anyone ever actually written a system (software or detailed explanation on paper with simple examples) that generates computer programs? I input $Prime(x) \wedge x<10$ and it creates a program that lists the prime numbers less than 10. $Prime(x)$ is simply defined as $$1<x \wedge \not\exists A\; s.t. 1<A \wedge A<x \wedge x=A\times B,\mbox{ with } A,B\in \mathbb{N}$$ Professors say they can but nobody gives actual complete examples.

• You mean like, you know, a compiler for a general purpose programming language? – Sasho Nikolov Mar 2 '14 at 18:21
• Hi - welcome to cstheory! Unfortunately your question is not a research level question in theoretical computer science and is off-topic on this site. – Lev Reyzin Mar 2 '14 at 19:43
• Actually, this is a good question, at the top of current research, and very promising. However, it is often very hard to specify precisely what you want. If you manage to specify it, then you need a system that will prove that it makes sense, that it is feasible, and that will require a mathematical proof. From that proof a program doing it can be extracted. But research for automating the proof and the program extraction is still in infancy, though making nice progress. You may look for example at Coq on wikipedia.- - - cc @LevReyzin – babou Mar 2 '14 at 23:56
• Here is a book corresponding to your question. There are others. It is not simple to understand. The Coq and Isabelle (another such system) crowd does include SE users who could give you more information and examples if the question were not closed. I found it by searching the web for: coq example program synthesis. – babou Mar 3 '14 at 12:55
• The area of computer science that captures what I you're asking about is called program synthesis and is an active area of research. – Huck Bennett Mar 3 '14 at 22:08

This is a very active research topic, very promising, though full automation of program generation probably has intrinsic limitations (but are human beings any better?). But the idea is still be very useful in assisting considerably the creation of programs by mechanizing many steps, and by automatically checking the correctness of the program generation.

It is strongly related to a result in logic, called the Curry-Howard correspondance (or isomorphism), that shows that computer programs and mathematical proofs are very similar.

So the idea is that the system will take your program specification as a theorem to be proved. In the case of your example, it would be something like (informally): "there is a set of all prime numbers smaller than 10".

Then, you will attempt to prove that theorem, and existing systems will assist you in doing the proof, automating some parts, possibly the whole proof, and making sure you never make errors.

From that proof one can then extract a program that actually computes the wanted list of prime numbers that had been initially specified.

Several systems were developed in the past to elucidate these ideas. One of the better known was LCF by Robin Milner, who created the language ML for that purpose. One of the currently most advanced systems is Coq.

There are examples fully worked out, some of them quite complex. You may find some in the following article, though it is in no way simple reading and requires advanced knowledge of Logic.

The wag answer: Yes, but at the time of writing, for most nontrivial programs the specifications seem to be just as hard to write and debug as the programs would be.

More seriously, babou's answer is good, but I'm also going to suggest checking out the area of dependent types. There's a rather good book using Coq (full disclaimer: written by a friend of mine), but there's also Epigram, Agda, and Idris. Isabelle/HOL is also worth checking out.

These are all based on the calculus of constructions. If you want to know the theoretical basis, look up Martin-Löf type theory. There are some great introductions around.

• I fully agree regarding specifications (and also the rest of your answer, but you know it better than I do). Any real programmer knows how difficult it is to fully specify what a program should do. It is a major issue in software engineering. And that translates also here, even though the problems addressed are more mathematical in general. However, I did not want to sound too discouraging (especially given the history of this question, illustrated by the first comment). – babou Mar 4 '14 at 13:06

Going off in a tangent here, program generators (i.e., systems that given a high-level description of something in some special language) have been around forever. Any compiler is one of those, as is any of the many parser generators. Back in the day systems called "third generation languages," which generated (most of the) code of a typical business application given a high-level description and a catalog of available data were popular.

Logic Programming and, more generally, Declarative Programming take as a premise exactly what you propose: namely, from a logical specification, return a result fulfilling that specification.

One area which seems to specifically address the "primes less than 10" example you give is Constraint Programing which tries to find solutions to problems involving certain constraints, including integer constraints like those you gave.

You might want to try ECLiPSe for a specific (open source) implementation of such a system.

• Would it be correct to say that the logic/constraint paradigm is more to specify answers than to specify programs. Of course, you might say that an incomplete specification is a program. But somehow, I am not sure it is the same game as program synthesis. It is true though that it does answer the example, because the example was very simple. I do not mean to say that constraints programming is only for simple problems. – babou Mar 5 '14 at 23:28