Program synthesis has been a dream of computer science for over thirty years. Today, the growing maturity of verification technology and the power of modern computers are finally bringing the dream closer to reality.
However, making synthesis practical requires us to rethink the relationship between the synthesizer and the programmer. For example, to cope with the daunting complexity of the synthesis process, all synthesizers must rely on human insights, often encoded as heuristics or domain theories. The key for practical synthesis is to allow programmers to provide these insights without the formal reasoning involved in axiomatic formulation. Additionally, programmers often want control over the details of their implementation. Practical synthesis technologies cannot take this control away from programmers.
Sketching is my answer to the challenges of practical synthesis. Sketching is a form of synthesis whose key novelty is the use of partial programs (sketches) to communicate insight to the synthesizer.
The talk will describe sketching as implemented in the SKETCH language, and the innovations in inductive synthesis that made sketching possible. The talk will also illustrate how sketching systems can be specialized to incorporate domain specific knowledge via problem reduction. Finally, the talk will describe our experience using SKETCH to synthesize complex implementations of ciphers, scientific codes, and even concurrent lock-free data-structures.
Armando Solar-Lezama is a student of Rastislav Bodik at UC Berkeley working on software synthesis. His main interests include programming languages, compilers and parallel computing. Before coming to Berkeley, he completed BS degrees in Math and CS at Texas A&M University, where he also worked as a programmer writing massively parallel neutron transport simulations.
His broad agenda is to exploit the growing availability of computing power and the increasing maturity of formal methods to make programming easier.