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