josef.win...@email.de writes:
> Right, a varified full flaged OS is still future.
> But there is nevertheless progress and affort.
Thanks for the pointeres, but anytime this comes up, an old AI
witticism turns up at the back of my head,
"If our mind were so simple we could actually understand it
fully, we almost certainly couldn't be bothered to try"
(original source lost or not within reach of my puny attempts at web
search). The point is, formal verification is *hard*, and any flaws in
your formal verification procedure will put you back at essentially
square one, every time. Which will happen a lot when exposed to
systems that have developed in response to real-world needs and formal
standards specifications that at least in some cases more likely than
not were in any way verified even to be internally consistent.
My money is still on the OpenBSD-style source code audits (aka
'reading the code like the devil reads the bible' for real-world
results.
- P
--
Peter N. M. Hansteen, member of the first RFC 1149 implementation team
http://bsdly.blogspot.com/ http://www.bsdly.net/ http://www.nuug.no/
"Remember to set the evil bit on all malicious network traffic"
delilah spamd[29949]: 85.152.224.147: disconnected after 42673 seconds.
