Programming by sketching

In software synthesis, the programmer doesn't write the code; instead, he gives the properties of the desired code and the code is automatically generated for him. The goal of the Programming by Sketching project is to make software synthesis practical and use it to improve programmer productivity and software quality.

We are currently exploiting code synthesis in two settings:

In implementation sketching, we synthesize provably correct high-performance cipher implementations: the programmer specifies (i) a reference specification of the cipher and (ii) a sketch of the cipher implementation—a sort of program with holes; the compiler then synthesizes the details omitted in these holes. The completed sketch is guaranteed to implement the reference cipher, allowing the programmer to explore clever implementation ideas without worrying about introducing bugs and without reasoning about tedious details. Read more.

In the Prospector project, code synthesis is used by a programmer's "search engine" to consolidate the results of its search into a code fragment that can be directly inserted into the code being developed, essentially while the programmer is typing. Prospector, our search engine, mines a code base with the goal of facilitating reuse of complex object-oriented frameworks. To obtain the code needed to reuse some functionality, the programmer only needs to state a "have" type A and a "want" type B (a surprisingly versatile query), and Prospector will compose the code that computes a B object from an A object using the code available in the framework. Read more.