Programming by Sketching

Опубликовано 6 сентября 2016, 5:45

When code is synthesized from a concise specification, the result is less coding and more correctness. Sketching seeks to bring synthesis to everyday programming by allowing to sketch the desired code, which guides the typically naive synthesizer. I will present two very different instances of sketching: a system for cipher programming and a synthesizing programmer's search engine. StreamBit: Programmers first write a clean reference of the cipher and then obtain a high-quality implementation by simply sketching the outlines of the desired implementation. The compiler fills in the detail missing in the sketch by ensuring that the completed sketch implements the reference code. The sketching compiler rejects buggy sketches, thus providing correctness by construction and allowing the programmer to quickly evaluate sophisticated implementation ideas. Prospector: Reusing code is hard because APIs are complex and their client code is often difficult to write. Prospector is a programmer's search engine that, given a query expressing the coding intent (a sketch), synthesizes the code ready for insertion into a program. The enabling innovation is the jungloid, a code pattern that covers many API coding headaches. I will explain how jungloids lead to simple search queries, how jungloids are mined, and how Prospector synthesizes jungloids it has never seen in the mining corpus. Joint work with David Mandelin, Armando Solar-Lezama, Lin Xu, (Berkeley), Rodric Rabbah (MIT), Kemal Ebcioglu, Doug Kimelman (IBM).