Lesson 12: Program Synthesis

• discussion
• video
• Program Synthesis is Possible
• Building a Program Synthesizer
  James Bornholt, 2018
• Program Synthesis
  Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh
• tasks due December 14

Gist

Program synthesis is the lofty idea that we can automatically generate code that meets a specification. The "specification" in that sense admits broad interpretation: it might be a logical formula relating inputs to outputs, a reference program that you want an equivalent but faster version of, a few input/output example pairs, or even a natural-language description. In practice, program synthesis usually consists of some kind of search over a large space of possible programs to find one that meets the spec, often driven by some manner of automated theorem prover.

Program synthesis technology is not ready to replace all human programs with search algorithms (yet?!!?!). But it has yielded exciting results in constrained domains that are nonetheless useful: famously, spreadsheet formulas, for instance.

For this lesson, we follow my tutorial-as-blog-post entitled "Program Synthesis is Possible" that walks you through the construction of a minimal sketch-based synthesizer in Python using the Z3 SMT solver. The aim of this tutorial is demystification: program synthesis can seem magical, but the basics to get something simple working can be surprisingly simple. Synthesis is a rich tapestry of ongoing research, so of course state-of-the-art synthesizers get way more complicated than the one you'll build here, but the point is to prepare you to read papers that build on this deceptively simple, definitely-not-magical foundation.

Tasks

• Follow the synthesis tutorial in your favorite language to build a sketch-based expression synthesis engine. You can use Python and Z3 directly, as in Adrian's tutorial, or try Rosette, as in James Bornholt's tutorial.
• Add an extension to generate more complex expressions than the ternary and bit-shift expressions from the tutorial. Get creative!
• Write a couple of example sketches that show off your new language extension, and report on how hard it was to get the solver to discharge them.