Fiat: Correct-by-Construction and Mostly Automated Derivation of Programs with an Interactive Theorem Prover

To scale to ambitious software-development tasks, programming languages must provide features for abstraction and modularity. Large advances in programming productivity have often come via new features of that kind. This project investigates new program-structuring ideas based fundamentally on machine-checked mathematical proofs. More specifically, through the design of a prototype system Fiat within the Coq proof assistant, the project studies how to derive efficient programs automatically from logical specifications. Programmers may package new notations and associated styles of automation as libraries, and a single program may mix notations, automatically benefiting from the combination of all of their associated automation for deriving efficient programs. In this way, Fiat makes it possible to split a program into parts for functionality and performance, with strong guarantees that bugs in the performance parts can never violate the requirements in the functionality parts. The intellectual merits are widely applicable new ideas in modular program structuring, with strong formal guarantees of correctness. The project's broader significance and importance are based on the potential to improve programmer productivity dramatically, for software projects in a wide variety of contexts; and the project also studies how the idea of mostly automated refinement from specifications can be integrated into introductory programming and discrete-math classes, to drive home the value of logical notation in programming.

The primary case-study domain in the project is practical Internet servers, such as for domain-name lookup or delivery of electronic mail. The goal is to develop Fiat versions of these key services, deriving efficient executable code automatically. Past work on deriving data layers from specifications in the style of SQL is being extended, in addition to exploration of other domains for specification and automated derivation, such as synthesis of parsers from grammars, to use for the protocols that servers speak, the configuration files that they read, etc. Beyond studying how such new libraries may be constructed and composed, the project also investigates how to push the synthesis process to lower abstraction levels than in our prototype implementation, which generates functional programs. The improved Fiat system will derive assembly programs, enabling choice of more effective optimizations thanks to more direct control of machine resources, integrating with the Bedrock Coq library for verified multilanguage programming.