Bedrock: building a software platform with mathematically proved correctness theorems

Today there are many social costs arising from the complexity of software. Consider the example of "app stores" for mobile devices. Many users download and run many programs contributed by others whom the users have no reason to trust. Approaches to filter software with inappropriate behavior include best-effort manual code audits and run-time enforcement of coarse-grained security policies. These approaches routinely fail to catch dangerous programs, since analyzing serious code bases is highly non-trivial.

An alternative is to prove mathematically that programs behave themselves. Such theorems about one layer of a computer system can then be composed into theorems about the all-encompassing properties of higher layers. If the proofs are written in enough detail, they can be checked automatically with specialized software. As a result, consumers can run software with higher confidence than in today's mainstream, even with lower costs in labor for auditing and so forth.

My group has been working on a tool for building such formally proved programs:
http://adam.chlipala.net/bedrock/
There are many opportunities to contribute to the tool or to build specific verified programs. Domains we are thinking about include mobile applications, cloud computing, Web browser plugins, and safety-critical embedded platforms.

The project involves functional programming along the lines of Haskell, so that sort of experience or equivalent background would be very helpful.

Interested candidates may contact Adam Chilipala,adamc@csail.mit.edu.