Program synthesis

Program synthesis is a special form of automatic programming that is most often paired with a technique for formal verification. The goal is to construct automatically a program that provably satisfies a given high-level specification. In contrast to other automatic programming techniques, the specifications are usually non-algorithmic statements of an appropriate logical calculus.

The idea originated in the 1960s with the aim of using techniques from artificial intelligence to build an automatic programmer, exploiting deep connections between mathematics and the theory of programming. Lack of early success meant that the mathematical approach soon fell out of favour, and lack of immediate success with other techniques led to a drop in enthusiasm for AI in general (the AI winter of the 1970s). Although some researchers still work on formal approaches, more success has been obtained by combining pure deductive techniques with powerful heuristics, and limiting their application to specific domains.

Some feel that the concept of automated program generation often results in poor "factoring" of information. Known redundancy should be factored out, not introduced, it is said. However, sometimes specific programming languages are limited such that one has to introduce repetition of a concept or pattern in order to keep using the same language. Here is a simplified illustration of factoring:

Poor factoring: x = a + a + a + a + a

Good factoring: x = a × 5

Program generation tends to focus on automating the repetition seen in the first example, when a better approach could be to find a higher-order abstraction, which is multiplication in this case. Other examples include putting parameters into a file or database instead of inside application code.

The framework of Manna and Waldinger starts from a user-given first-order specification formula. For that formula, a proof is constructed, thereby also synthesizing a functional program from unifying substitutions. Proof rules include non-clausal resolution, logical transformations, splitting of conjunctive assertions and of disjunctive goals, and structural induction. Murray has shown these rules to be complete for first-order logic. In 1986, Manna and Waldinger added generalized E-resolution and paramodulation rules to handle also equality; later, these rules turned out to be incomplete (but nevertheless sound).

...
Wikipedia