To many people, program synthesis is the most exciting application area for AD in economic terms. The idea of presenting human-understandable task specifications to a computer system and receiving in return a program that is known to meet the specifications submitted is hard to fully appreciate, in terms of both the intellectual accomplishment represented and the economic impact such capability would have. Once achieved--and full realization of this dream is surely well in the future--all investment in AD will be repaid many times over. We note that this task is not isolated from other AD tasks, for work such as verification research moves forward the technology that program synthesis will (and does) exploit.
The output of a synthesis machine is no better than the quality of the specifications that are entered. Our earlier anecdote about the German network software makes clear the problem of assuring the correctness of specifications. Since developing specifications is formalizing the informal, there can be no formal proof of correctness issue here. One aspect to address is the design issue; human error will be minimized if the specification language is tailored to the task domain, particularly at the level of concept representation (``granularity''). The other major issue to address is tests of representation quality. Consistency of the specifications is one concern; this clearly uses AD technology. Another concern is semantic checks, meaning items from type checking to operational semantics for some constructs of the specification language. This research is under way, as examples cited earlier illustrate.
We address the future prospects of program synthesis in general by first commenting further on the KIDS project of D. Smith at Kestrel Institute. The KIDS program, together with the associated research effort, is a sophisticated example of the constrained program synthesis concept. Inference is used in a major way, but under the control of design tactics (plans) that are custom-built to the algorithm and problem classes within which the problem of interest falls. Problems are formally specified by giving information that includes an input domain and a notion of what constitutes a problem solution. This problem theory is fitted to an algorithm class. (Actually an algorithm theory extends the problem theory in the sense of adding appropriate logical structure including axioms about the algorithm class. This corresponds to constructing an interpretation between theories.) For example, there is the problem reduction algorithm theory that includes divide-and-conquer and dynamic programming algorithm theories in hierarchical fashion. The divide-and-conquer algorithm theory, when coupled with a problem specification for sorting integers, provides the structure to yield a quicksort algorithm. For an actual program this is all fit to a program theory that introduces the control and programming language chosen. The design tactics that control the inferencing are carefully tailored to the theories as they are developed. For example, the divide-and-conquer tactic will effectively produce a specific divide-and-conquer algorithm that is a model of the general divide-and-conquer theory. The design tactics have a constructive aspect that first allows a user to select standard components for parts of an algorithm and then has the inference system deductively solve for the remaining components by using the axioms of the algorithm theory.
We will not comment extensively on the other research in program synthesis and the opportunities there, as many of the critical technologies needed are those of other domains of AD and discussed under other areas. This is not to slight the need for other high-quality work within the domain of program synthesis. We have already mentioned the work of Manna and Waldinger as influencing the design of AMPHION. Good work on program synthesis has been done within the logic programming community [39]. We mention a problem area not yet named that is germane here, proof by analogy. This problem is usually associated with mathematical reasoning, but some researchers in software engineering, aware of the usefulness of AD, see a role for proof by analogy. The idea is to use interactive AD tools in program development in such a way that the specifications and program are constructed, or at least finalized, together. Thus one develops prototype programs and uses these to converge to the final product and its specifications. The proof by analogy is appropriate in the updating of correctness proofs that show that the implementation meets the specifications. Although efforts have been applied to the problem of proof by analogy, this appears to be one of the harder problem areas in this field, and substantial progress seems some distance away at present.