Read-Eval-Synth Loop: Synthesizing software

A frequent programming pattern for small tasks, especially expressions, is to repeatedly evaluate the programon an input as its editing progresses. The Read-Eval-Print Loop (REPL) interaction model has been a successful model for this programming pattern. We present the new notion of Read-Eval-Synth Loop (RESL) that extends REPL by providing in-place synthesis on parts of the expression marked by the user. RESL eases programming by synthesizing parts of a required solution. The underlying synthesizer relies on a partial solution from theprogrammer and a few examples.

RESL hinges on bottom-up synthesis with general predicates and sketching, generalizing programming byexample. To make RESL practical, we present a formal framework that extends observational equivalence tonon-example specifications.

We evaluate RESL by conducting a controlled within-subjects user-study on 19 programmers from 8companies, where programmers are asked to solve a small but challenging set of competitive programmingproblems. We find that programmers using RESL solve these problems with far less need to edit the codethemselves and by browsing documentation far less. In addition, they are less likely to leave a task unfinishedand more likely to be correct.

Source: Programming with a Read-Eval-Synth Loop, Peleg et al.