The long-term goal of our research is nothing short of automating programming. We imagine a world where humans would describe what computational tasks they want performed at the level of high-level insights and goals. Algorithms using large amounts of compute power and feeding on large amounts of data would figure out the low-level details of how the tasks are to be performed.
The word “synthesis” in “program synthesis” refers to this process of generating the how from the what. The word “program” is interpreted broadly, and includes, for example, fixes to programs and proofs of program correctness. While automating general-purpose programming is likely to remain a dream for a long time to come, we expect advances in program synthesis to slowly chip away at repetitive programming tasks, domain by domain.
The twin foci of our research are scalable algorithms for synthesis and related problems, and the language interfaces through which human users interact with these algorithms. Our preferred approach to research straddles theory and practice. We seek out research problems that are motivated by practical scientific and engineering challenges. However, our goal is always to produce foundational knowledge that cuts across instances and domains, and to build on and unify insights from the research areas of Programming Languages, Logic in Computer Science, and Artificial Intelligence.