On Tue, Sep 22, 2009 at 10:13 AM, erik quanstrom <quanstro@quanstro.net>wrote:

> > btw, there's even been one ukernel recently that has a formal
> > proof of correctness (against its specification and some containment
> > properties).  Roughly a 10 man-year effort for about 7.5kloc.
> > Not something you'd likely be able to do yet against something linux-
> > sized.
>
> the other way of looking at this is all the complex and error
> prone stuff is not prooved.
>
> i'm not clear on what all functional correctness entails.  can
> a functionally correct program suffer from deadlock or livelock?
>
>
I'm not sure... I can tell you when I spawn threads in haskell that, while
testing, the runtime seems to detect certain deadlock states, tells me about
them, and then the program crashes.  I like that a little better than
deadlock :-)

How that all works is a lit

Dave


> - erik
>
>