To those of you who may be interested, I’ll be defending my Ph.D. thesis (titled “Performance Engineering of Proof-Based Software Systems at Scale”, aka “Why is Coq so Slow‽ and How Do We Fix It?”) on Monday, November 30th at 11 am EST on Zoom. Anyone is welcome to attend; email me directly at jgross@mit.edu if you’d like the zoom link and password (not shared here to prevent zoombombing).
Abstract:
Formal verification that programs are bug-free and behave correctly is increasingly valuable as our world comes to rely more on software for critical infrastructure. A significant and under-studied cost of developing verification, especially at scale, is the computer performance of proof generation.
Over the course of my doctoral study, I’ve repeatedly run into performance issues in Coq. My thesis and defense are my attempt to synthesize my experiences into a coherent roadmap of performance bottlenecks in dependently typed tactic-driven proof assistants and to present significant developments I’ve engineered and techniques I’ve discovered over the course of my doctoral work.
I intend to present a broad overview of the main project I spent my Ph.D. working on, Fiat Cryptography, a verified code generator for low-level cryptographic primitives whose output is already being used in Google Chrome and other applications. This project will present the setting for the main technical contribution of my thesis, a verified framework that performs well at scale for code specialization, partial evaluation, and generic rewriting. Using as case studies the development of this framework, as well as my experience formalizing category theory and synthesizing verified parsers, I will present the metrics I’ve identified as most commonly being useful for predicting performance scaling in large-scale proof developments, together with brief explanations.
Recording will be made available. Thesis draft (still a work in progress) available upon request, and freely accessible before year-end, if all goes well.
-Jason