Abstract

The benefits of formal correctness proofs for software are clear intuitively, but the high human costs of proof construction have generally been viewed as prohibitive. The speaker believes that pervasive verification of deep theorems about software will never be common until formal methods are integrated within the software development process. To support that integration, we need to rethink the familiar programming toolchains. The new world needn’t be all about doing prodigious extra work to achieve the virtue of correct programs; formal methods also suggest new programming approaches that better support abstraction and modularity than do coarser-grained specification styles like normal static types.

This talk overviews Bedrock, a framework for certified programming inside of the Coq proof assistant. Bedrock programs are implemented, specified, verified, and compiled inside of Coq. A single program may be divided into modules with formal interfaces, written in different programming languages and verified with different proof styles. The common foundation is an assembly language with an operational semantics (serving as the trusted code base) and a semantic module system (orchestrating linking of code and proofs across source languages). A few different programming styles have been connected to the shared foundation, including a C-like language with an “array of bytes” memory model, higher-level more C++-like languages with “array of abstract data types” memory models, a domain-specific language for XML processing, standard Coq functional programs, and even declarative specifications that are refined automatically into assembly code with correctness proofs.

The talk will present Bedrock’s shared foundation and sketch the pieces that go into refining declarative specifications into closed assembly programs, covering joint work with Thomas Braibant, Santiago Cuellar, Benjamin Delaware, Jason Gross, Gregory Malecha, Clément Pit—Claudel, and Peng Wang