Conclusions on Program Synthesis from Axiomatizations

The other major problem with deductive synthesis is related to the formality of the specifications. Where do the formal specifications come from If deductive synthesizers guarantee total correctness of the resulting algorithms with respect to their specifications, what guarantee do we have that these specifications correctly capture our intentions These questions are often either dismissed as irrelevant or considered as intractable issues that are left for future research. But what use are these synthesizers if we don t even know whether they solve our problems or not See [Le Charlier 85] and [Flener and Popelmsky 94] for a detailed discussion of this controversial topic. 

Inductive inference is not so common in automatic programming. We first define, in Section 3.1, the underlying specification formalism, namely examples. In Section 3.2, we present the major results about inductive inference. Then, in Section 3.3 and Section 3.4, we survey the synthesis of functional programs from examples, and the synthesis of logic programs from examples, respectively. Finally, in Section 3.5, we draw some conclusions on the use of inductive inference in automatic programming. 

---