Functional and Logic Programming

The twenty-first century has seen an exciting uptick in the use of proof assistants for mechanized correctness proof of realistic computer systems. That is, developers are not just writing code but also using software tools for writing and checking proofs, establishing that code behaves as it should, increasing assurance dramatically compared to alternatives like testing. These developments, using proof assistants like Isabelle and Coq, exhibit widely varying levels of proof automation. That is, the individual steps of logical arguments come at very different levels of detail, from “now apply modus ponens” to “now establish the correctness of this whole phase of my compiler, through the following several pages of heuristic scripting.” Increased levels of automation seem important for more widespread adoption for proof of real-world systems, to overcome doubts that mechanized proof adds too much developer effort. This talk will give my reections on trying to scale up automation in the Coq proof assistant, and I hope, also provide lessons relevant to other proof assistants. My collaborators and I have found that almost any serious effort of this kind is likely to hit a performance wall, with Coq as it stands today. The existence of such a wall may surprise Coq users who are accustomed to writing more manual proofs, roughly at the level of careful paper proofs; and it may be all the more surprising to those who think of any kind of “proof” as inherently theoretical and thus disconnected from concerns of performance optimization. I will give examples in proof of functional correctness for software and hardware systems. What are the key challenges? In the tradition of dependent type theory that Coq builds on, term reduction is a central operation of proof checking, and reduction strategies matter a lot for performance. Coq users can learn about the intricacies of how the proof checker chooses strategies, or they can be more explicit through methods like proof by reflection, one successful example of which I will describe. On top of the core mechanics of proof checking, a proof assistant will typically provide a proof engine that exports higher-level operations managing subgoals and unification variables. We have been studying the fundamental determinants of poor performance scaling by Coq’s proof engine, and I will sketch preliminary results on bottlenecks in key operations. My overall goal in the talk is to make clear that these performance issues are underappreciated but crucial to scaling proofs. As a community, we are evolving proof assistants and their applications in tandem, learning lessons about the design of both. No doubt today’s performance bottle-necks will be addressed by a mix of “mere engineering” and new scientific contributions, and I would like to encourage the audience to consider looking into both!