I’m be up front about it… I love the idea of formally verifying the semantics of a program.
When I was a little younger, I was really fascinated by the idea of using standard mathematical techniques to prove that a program did what it claimed to do. Moreover, the idea of using constructive mathematical logics to extract computational meaning from proofs, seemed almost magical to me. This latter area is summarised nicely in a recent paper by Robert Constable. I started working on a Phd in this area and spent some time working with Martin-Lof type theory inside Isabelle. At one point, I was offered the chance to prove the correctness of a washing machine controller as a thesis topic.
It was therefore interesting to see the recent channel9 interview with Chris Hawblitzel on Verve, a verified kernel for a single processor operating system. This is really interesting work which is covered in the paper. The idea is that a small amount of x86 machine code (the nucleus) is verified using Hoare logic. This is then used to execute C# programs which have been compiled down to typed assembled language. Typed assembly language is covered in this paper, and the author goes into a lot of detail about verifying two garbage collection algorithms in this paper. The last paper is really interesting in that the authors didn’t use an interactive theorem prover, but used a system that derived verification conditions from a high level language (BoogiePL) representation of x86 instructions. They needed to provide hints to the theorem prover about which definitions with universal quantifiers needed expanding (the T function of the paper), and used regions to convert global theorems into local theorems that the prover could solve. After the correctness proof, the x86 code could be automatically generated.
The system doesn’t yet support more interesting constructs such as exceptions and multiple processors, but this is great foundation work that will surely be improved in the future.