The long-term goal of our research is to automate significant parts of what’s understood today as “programming”. We imagine a world where humans won’t need to code up implementations of computational tasks in gory, low-level detail. Instead, they would express their usually-partial, possibly-ambiguous understanding of what these tasks are, using notations ranging from test cases to constraints to natural language. Algorithms using large amounts of compute power and feeding on large amounts of data would interpret these specifications and figure out how to realize them as code.
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, and vastly increase programmer productivity in the process.
The two foci of our research are scalable algorithms for synthesis and related problems, and practical tools through which these algorithms can be embedded in a software engineering workflow. 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.