Hila Peleg
Talk: Programmer-driven program synthesis
- Date and Time
- May 7 at 10am
- Location
Abstract
Recent years have seen great progress in automated synthesis techniques that can automatically generate code based on some intent expressed by the user, but communicating this intent remains a major challenge. When the expressed intent is coarse-grained (for example, restriction on the expected type of an expression), the synthesizer often produces a long list of results for the user to choose from, shifting the heavy-lifting to the user. An alternative approach is programming by example (PBE), where the user leverages examples to interactively and iteratively refine the intent.
Existing program synthesis tools are usually designed around the synthesizer and its internals. However, these are tools intended for users, who are the ones who must specify (and respecify) the specifications. Synthesis tools are often designed either with no particular group of users in mind, or with the purpose of generating code for users who cannot write and read it.
We suggest instead designing synthesis tools specifically for programmers. This allows making assumptions on both the input the user can generate and the output they can consume. Concepts that are part of the programmer’s life such as code review and read-eval-print loops (REPL) can be leveraged. But this approach also brings with it restrictions for the synthesizer, which pose new design challenges: examples, a common tool, are not expressive enough for programmers, who can observe the generated program and refine the intent by directly relating to parts of the generated program. Additionally, can the users correctly judge when the program is correct?
Synthesis is, at best, a computationally hard problem. Designing for the user can put the interface of the synthesizer at odds with state of the art synthesis techniques. We show how a set of code-review-like predicates interfere with observational equivalence, one of the corner stones of synthesizer implementations. We modify observational equivalence to adjust for this problem, and discuss the importance of designing for the user and synthesizer in parallel.
This talk is based on joint work with Shachar Itzhaki, Sharon Shoham, and Eran Yahav.
Bio
Hila Peleg is a doctoral researcher in the Department of Computer Science at the Technion, advised by Eran Yahav. She also holds a degree in literature. She is currently researching interaction models between programmers and synthesis procedures.