Exploratory Phenomena in Program Synthesis
Program synthesizers promise to save time for the programmer by writing parts of their code for them, provided the programmer knows exactly what they want. For it to suggest that code, the programmer must convey the nuances of their specification to the synthesizer. Is there a place for program synthesizers when those nuances are unclear, and a programmer must explore the design space of their problem? This dissertation argues that program synthesizers can facilitate exploring for code, and that techniques to validate explored code are needed to reduce cognitive effort.
To use a traditional synthesizer successfully, the programmer needs a deep understanding of the problem. Firstly, a programmer must convert their intent into the specific language their tool understands, which may not match how they think about their intent. Secondly, a programmer needs to know all the edge cases of their problem and how each one should behave. If both of these cannot be met, then a traditional synthesizer will usually be more effort to use than simply writing the desired program.
As modern, probabilistic synthesizers require less overall information to offer a suggestion, they can fill a new role in the programming workflow: code exploration. A programmer no longer needs complete understanding of their problem nor be able to communicate all nuances to the tool. This new exploration domain presents new challenges, particularly one of validating the code matches the often incomplete intent of the programmer. Validating code against intent must be quicker or easier to justify a tool’s use in exploration to be useful. In this dissertation, I show that both traditional and probabilistic program synthesizers can aid in this exploratory process of programming, and that techniques to validate that explored code reduce the cognitive effort.