Program Synthesis

The problem of "automatic programming", i.e. the attempt to implement a software system where one just "says what one wants" and then the program one wants gets written automatically is tempting but in its generality extremely difficult to achieve.

Nevertheless partial and constraint approaches towards so-called program synthesis have been investigated since the late 1960s and doubtless did achieve acceptable results, though - arguably - not yet a breakthrough. One line of approach is to restrict the problem: Instead of trying to create a program out of thin air, from scratch it seems more feasible to start from a partial program "sketch" and to just fill in certain aspects, parameters, statements, etc.

Questions which arise include: How to specify what one wants? (i.e. program logic similar formalisms used in verification). This is especially interesting when it comes to non-functional e.g. performance or security or other quantitative, properties.

How to specify partial solutions of a synthesis problem, program sketches etc. In particular in this context the usage of probabilistic sketches which allow us to embed discrete structures (the syntax trees of a program or sketch) in a continuous manifold (leading perhaps to a differntial geometry of programs?).

How to obtain a final result which exhibits certain properties, may they be functional or non-functional, this always boils down to finding a solution or at least an optimum (especially for performance aspects and similar). The main aspect would be to study (non-linear) optimisation techniques in order to construct the required solution or approximate an optimum.

What can be guaranteed about the time it takes to find a solution or optimum? How precise is the solution? How stable is it - i.e. what happens when the specifications change slightly? etc.