##
A Framework for Quantitative Program Synthesis

### Herbert Wiklicky

We present a methodology which recasts program synthesis problems in a
purely quantitative framework based on concepts in continuous
(non-linear) rather than discrete optimisation. The first element of
this is the representation of the semantics of deterministic (and
probabilistic) programs as linear operators, or in the finite case
simply as matrices. This allows us to identify (probabilistic) program
sketches or, to be precise, their semantics as elements of an
appropriately parameterised manifolds of such operators. The synthesis
problem can then be interpreted in this setting as a non-linear,
global optimisation problem. We illustrate this approach via a number
of examples which involve functional as well as non-functional program
properties.