From mboxrd@z Thu Jan 1 00:00:00 1970 From: erik quanstrom Date: Tue, 22 Sep 2009 13:13:16 -0400 To: 9fans@9fans.net Message-ID: In-Reply-To: <> References: <> MIME-Version: 1.0 Content-Type: text/plain; charset="US-ASCII" Content-Transfer-Encoding: 7bit Subject: Re: [9fans] linux stats in last year from linuxcon Topicbox-Message-UUID: 7540936a-ead5-11e9-9d60-3106f5b1d025 > 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