University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Bedrock: A Software Development Ecosystem Inside a Proof Assistant

Bedrock: A Software Development Ecosystem Inside a Proof Assistant

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

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

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity