Provably correct microkernel (seL4)

[Kevin.Wall at qwest.com (Wall, Kevin)]

Thought there might be several on this list who might appreciate
this, at least from a theoretical perspective but had not seen
it. (Especially Larry Kilgallen, although he's probably already seen it. :)

In http://www.unsw.edu.au/news/pad/articles/2009/sep/microkernel_breakthrough.html,

    "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."

In a new item at NICTA
<http://nicta.com.au/news/current/world-first_research_breakthrough_promises_safety-critical_software_of_unprecedented_reliability>

it mentions this proof was the effort of 6 people over 5 years (not quite
sure if it was full-time) and that "They have successfully verified 7,500
lines of C code [there's the problem! -kww] and proved over 10,000
intermediate theorems in over 200,000 lines of formal proof". The proof is
"machine-checked using the interactive theorem-proving program Isabelle".

Also the same site mentions:
    The scientific paper describing this research will appear in the 22nd
    ACM Symposium on Operating Systems Principles (SOSP)
        http://www.sigops.org/sosp/sosp09/.
    Further details about NICTA's L4.verified research project can be found
    at http://ertos.nicta.com.au/research/l4.verified/.

My $.02... I don't think this approach is going to catch on anytime soon.
Spending 30 or so staff years verifying a 7500 line C program is not going
to be seen as cost effective by most real-world managers. But interesting
research nonetheless.

-kevin
---
Kevin W. Wall           Qwest Information Technology, Inc.
Kevin.Wall at qwest.com    Phone: 614.215.4788
"It is practically impossible to teach good programming to students
 that have had a prior exposure to BASIC: as potential programmers
 they are mentally mutilated beyond hope of regeneration"
    - Edsger Dijkstra, How do we tell truths that matter?
      http://www.cs.utexas.edu/~EWD/transcriptions/EWD04xx/EWD498.html