> 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? - erik
