christopher.lord.ac

christopher.lord.ac

Christopher Lord  //  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.

Sep 23 / 8:27am

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. 

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.
Loading mentions Retweet

0 comments

Leave a comment...

 
To leave a comment on this posterous, please login by clicking one of the following.
Posterous-login     Connect     twitter