Program Synthesis with Lightweight Abstractions

Abstract

The world is reliant on software systems of unprecedented scale,while our methods for developing software still require programmers to manually write code with little help toward ensuring the software correctly meets its intent. Program synthesis, which automatically generates correct programs from specifications, offers a hopeful path forward. While program synthesis has had many successes in recent years, these have mostly been in restricted domains; synthesis has not yet proved useful for the practicing software engineer.

This dissertation aims to advance program synthesis to meet thechallenges posed by the use of modern general-purpose languages, tools, and frameworks. This dissertation presents work towards an automated programming stack that uses specifications and expressive test cases written by programmers to scale synthesis tools to diverse domains. Specifically, it demonstrates that types enriched with effect descriptors inferred from test cases are a potent means to guide the synthesis of real Ruby on Rails web apps, and that types enriched with logical predicates can be used to synthesize verified privacy preserving queries. The key to both projects, and most other successful synthesis work, is the proper choice of abstraction for the problem domain at hand. Based on this insight, this dissertation contributes a new synthesis framework that takes as a parameter an abstract interpreter and automatically guides the search with it. This framework captures many different synthesis approaches from the literature, making it easier to build the synthesis tools of the future. The dissertation concludes with a vision for an automated programming stack that uses specifications and expressive test cases written by programmers to scale synthesis tools to diverse domains, moving us closer to a world in which correct programs are constructed automatically based on programmer's intent.