Calibrating Research in Program Synthesis Using 72,000 Hours of Programmer Time

After the initial enthusiasm of the ’70s and ’80s abated, the topic of program synthesis is now being researched with renewed inter-est. Recent advances can be explained in large part by significant strides made in automated theorem proving technologies, partic-ularly in the development of satisfiability solvers. In an effort to understand the scalability of program synthesis, we ran a three-day programming contest featuring thousands of expert programmers. The results of the contest were astounding: the winning teams pro-duced program synthesizers that scaled several orders of magnitude beyond the current state of the art in the research literature. In one sense, this is a “reality check ” for program synthesis researchers. In another, this is cause for great optimism—program synthesis has the potential to scale well beyond what we thought was possible, if only we are willing to fine tune and employ strategies that were previously thought infeasible. A note from the authors: The first six authors are all members of “Unagi—The Synthesis”, the team that won the ICFP program-ming contest 2013—we refer to them collectively as “Unagi”. The last two authors organized the contest and prepared this report, based, in part, on communications with Unagi