Adam Chlipala
Talk: A Case for Integrating Proof Assistants into Daily Programming
- Date and Time
- April 26, 2017 at 3:30pm
- Location
Abstract
Computer proof assistants are IDEs for developing rigorous mathematical proofs that are checked algorithmically. They are just beginning to be accepted as useful for “real work” in domains from systems infrastructure to applications. Still, most observers think of a mechanized proof as a kind of penance that programmers can pay to be especially virtuous. Are machine-checked proofs just an extra cost, bolted on to a standard software-development process, to increase assurance? I will argue that, instead, mechanized proofs are a key enabler of new patterns of abstraction and modularity, and these new patterns deserve to permeate the whole life cycle of development.
I will draw examples from a few different efforts I’m involved with, applying the Coq proof assistant. One reach target, for the different aspects combined, is to synthesize efficient and secure Internet servers from specifications. Key challenge areas included persistent data management, parsing of network wire formats, and cryptography. I will describe how we are able to generate performance-competitive code automatically from reasonable specifications in each domain – and how to do it in a way that generates proofs of correctness. The resulting programmer experience is something between “program synthesis” and “programming with well-designed libraries.” The paradigm we’re pushing is code libraries that include specification notations and procedures that know how to compile those notations efficiently, with proofs.
Bio
Adam Chlipala has been on the faculty in computer science at MIT since 2011. He did his undergrad at Carnegie Mellon and his PhD at Berkeley. His research focus is applying mechanized logical reasoning to the programming process (both software and hardware) to improve how we implement, compile, specify, verify, and synthesize code. Much of his work uses the Coq proof assistant, about which he has written a popular book, “Certified Programming with Dependent Types.” Current projects involve verification and synthesis for processors, file systems, cryptography, databases, and Internet servers. He is designer and implementer of the Ur/Web programming language, a domain-specific functional language for building modern Web applications, which has a few commercial users.