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

[Dustin Getz <dustin.getz@gmail.com>]

great links, Ben -- thanks for sharing!

Dan, i reflected on your comment:

> haskell has features that make it easier to do proofs of correctness, be 

secure and and to clearly enunciate your thoughts. This is if you think 
about it,  very anti-agile and does require alot of up-front design.

my thoughts are still unclear, but i actually think haskell might be perfect for agile:

1) the "up front design" that haskell forces, means future sprints don't have to clean up a bloody mess to before adding features.

2) haskell's vigorous types give us "the ability to make a large change that will affect the structure of your code, and know for sure that you’ve hit all the places where that change makes a difference. Indeed, the type checker can direct your attention to what remains to be updated."[1]

i think we're totally on the same page here, we're just looking through slightly different lenses, both of which are fair. cheers.

[1] https://plus.google.com/116635422485042503270/posts/CyaSB5qRXY7

p.s. anyone use g+?

On Wed, Oct 5, 2011 at 1:10 PM, Ben Karel <eschew@gmail.com> wrote:

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