Programmers have resigned themselves to an awkward situation: practical code intermingles functionality and performance optimizations, in a way that makes both harder to understand. I will present our system Fiat for untangling those threads, generating efficient code automatically from mathematical specifications. Fiat is both foundational, as every code generation outputs a Coq proof of correctness, and extensible, as programmers may create libraries with new strategies to translate specification patterns into code patterns.

We approach the design of Fiat more like the design of a programming language than of an automated theorem prover: the goal is to craft a minimal yet powerful core of features for expressing specifications, efficient programs, the rules that transform the former toward the latter, and the proofs that justify the rules. Beyond what is built into Coq, the most central abstraction is nondeterministic programs as sets of possible outcomes, with a classic refinement relation formalizing what it means to commit to a design decision that reduces nondeterminism. We also work with a core concept of stateful abstract data types, with private state and (nondeterministic, possibly even uncomputable) methods. On this foundation, we build an ecosystem of libraries for different specification styles, including relational queries for data management and grammars for parsers.

I will describe the conceptual foundations and demo the system in action, both for small tutorial-style examples, walking through step-by-step derivations, and for more complete case studies, using the full degree of automation.

Adam Chlipala finished his BS in computer science at Carnegie Mellon in 2003 and his PhD in computer science at UC Berkeley in 2007. Before starting at MIT, he was a postdoctoral fellow at Harvard. His research focuses on applications of formal logic to software development and analysis. One specialty area is building machine-checked mathematical proofs of correctness for programming tools like compilers and runtime systems, and he has a general interest in the pragmatics of machine-checked mathematics. He also works in the design and implementation of functional programming languages, as in the example of his new domain-specific programming language Ur/Web, which brings strong mathematical guarantees to the world of Web applications.