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