This class is about building programs with machine-checked proofs of functional correctness. Techniques like model checking enable mostly-automated verification of shallow properties of deep programs. Our focus in this class will be on verifying deep properties of small- to medium-sized programs, using interactive proof assistants. In particular, we will focus on the Coq proof assistant, which, together with its associated tools, serves as a (perhaps surprisingly, to most people) quite mature development environment for programming with specifications. The goal of this class is to convince you that you (yes, you!) can start using Coq today to build verified programs, with an increase in effort over traditional programming that is justified by the formal correctness theorems you end up with.
The focus of the class will be on engineering best practices for certified programming and interactive theorem proving. Just what these practices are is far from a settled question, but we'll do our best to maximize programmer/prover productivity and promote readability and maintainability of the results. We plan to push one particular recipe for this that almost no one is using yet: dependent types plus custom-tailored proof automation.
Dependent type systems allow types that refer to programs. The possibilities of this idea are pretty mind-boggling, ranging from assigning array deference a type guaranteeing no out-of-bounds references, to assigning a compiler a type that guarantees that its output programs have the same observable behavior as its input programs. Putting dependent types to use requires a lot of theory, a lot of tool construction, and a good amount of experience with basic "design patterns." Luckily for us, Coq already provides the first two. One of the big aims of this class is to provide the third.
With dependent types, you can often "prove" important properties of your programs with almost no additional effort beyond writing the program normally, when you manage to find appropriate dependent types to assign. When this works, what you've discovered is that there is a correctness proof that mirrors the structure of your program. For many interesting verification problems, no such proofs exist. For instance, a compiler correctness proof must follow the structure of program executions, which may follow neither the structure of the compiler nor the structure of the programs it processes.
Coq provides a very general "proof script" facility for writing out manual proofs of such theorems. It's a safe approximation to say that any mathematical proof can be formalized in this way. Most of the current and historical work with proof assistants for higher-order languages has used very manual proof approaches. With proof assistants like Coq and Isabelle/HOL, we have "proof by video game," where the human prover alternates between reading dumps of proof state and entering short commands to simplify the goal. The final results tend to be impossible to understand without replaying the proof step by step. With proof assistants like Twelf, the situation is worse for initial proving, as the proofs people write in practice are essentially isomorphic to formal natural deduction proofs in full gory detail. The results are more structured and thus more readable in that sense, but the extreme level of detail can be just as confusion-inducing as extreme lack of structure.
In this class, we'll focus instead on a style that we call "proof by decision procedure." Coq includes a Turing-complete language for writing programs that manipulate proof states, such that, by construction, one of these programs can never claim to have proved a goal when it really hasn't. We will show how many examples of certified programming can be completed by writing custom decision procedures that are robust to changes in program implementation and specification. Proofs in this style are naturally decomposed into pieces that can be read and understood in isolation, free of deep hierarchical structure, a major victory for maintainability.
We expect to spend almost all of class time on example programs and proofs, with the class working together to build the solutions in a live Coq environment. We'll draw examples from a variety of domains, based on audience interest. We'll probably spend a good amount of time on applications related to certified programming language tools, since they provide a great stress test for reasoning about programs with complicated specifications, and also because the instructor thinks they're cool. We also hope to spend a lot of the class on case studies suggested by participants based on their own research and other interests.
================================================
Topics to cover in whole class periods or longer
================================================
* A simple compiler from a binder-free language to a stack machine, and its mostly-automated proof
* Crash course on basic tactics for manual proofs
* Crash course on induction and its pitfalls in Coq
* Infinite data objects and proofs via co-inductive types
* Programming with subset types and refinement
* Introduction to more dependent types
* Alternatives for defining dependent datatypes
* Introduction to Ltac, Coq's Turing-complete tactic language
* Pattern matching and backtracking in Coq tactics
* Proof by reflection (AKA putting certified decision procedures to work)
* Proving things about programs that use type equality proofs
* Techniques for representing variable binders
* First-order techniques: concrete names, De Bruijn indices, locally nameless
* Higher-order abstract syntax, and how to get most of its benefits in Coq
