Provably correct microkernel (seL4)

[ljknews at mac.com (ljknews)]

At 4:33 PM -0500 10/1/09, Wall, Kevin wrote:

>     "Professor Gernot Heiser, the John Lions Chair in Computer Science in
>     the School of Computer Science and Engineering and a senior principal
>     researcher with NICTA, said for the first time a team had been able to
>     prove with mathematical rigour that an operating-system kernel -- the
>     code at the heart of any computer or microprocessor -- was 100 per cent
>     bug-free and therefore immune to crashes and failures."

Reading nothing beyond what was posted, the problem I see is
to provide a complete specification against which to prove
correctness.
-- 
Larry Kilgallen