Formal Verification and Haskell

In this paper on formal verification of seL4, the authors construct a proof of an operating system kernel. I suggest you at least skim the paper. 

Pastedgraphic-1

I've been investigating using techniques like this for formally implementing computer languages from their standards. The process would consist of taking the standard, and applying a minimal transformation to Haskell. From this formal implementation, one can derive an optimized implementation, if the Haskell code is not sufficiently performant.

This is a very strong strength of functional languages. One can say something about them based on formal reasoning. I'll follow up with examples of how to apply this technique to specifications.

About

I work on compilers for a major corporation, specialized in computer languages and the parsing and optimization thereof. In my spare cycles I hack on Haskell, Ruby, and Objective C. Outside of programming, I am an outdoorsman, a skilled photographer, a student of typography and design, and a patient, better driver. buzz.

TwitterFacebookFlickrVimeo