Re: haskell -- very frank HN discussion about haskell's alleged "impedance mismatch"

[Ben Karel <eschew@gmail.com>]

On Wed, Oct 5, 2011 at 12:52 PM, Dustin Getz <dustin.getz@gmail.com> wrote:

i wonder what the state of the art is in terms of proving the haskell runtime? i wonder if anyone proves their program, then meticulously translates it into C.Â

The state of the art is just starting to tackle verification of (simplified versions of) individual components of modern language runtimes. As one example, the systems lab at PSU has a year-old paper on certified GC:Âhttp://web.cecs.pdx.edu/~apt/icfp10.pdf

There's also a two-year old paper on a verified OS microkernel, which involved a proof of correspondence between hand-written C and a formal executable spec:Âhttp://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf