On 9/19/13 9:29 PM, josef.win...@email.de wrote:
Does OpenBSD plan to varify its (main) components, to reach the level of zero-bug software?
I do assume that you are talking about "formal verification" meaning "mathematical proof of correctness".
Verify against what? Verification is a binary mathematical relation between a formal specification and an implementation. So, to start you need a specification. I have never seen a specification of a UNIX-like operating system that can claim completeness is any way. And if there was, it may contain as many bugs as the code. This is a dead end ...
Instead what you normally do is formally verifying certain, small aspects, like "are all variable initialized" or "will I ever be able access unallocated parts of the memory". Interestingly enough, whenever such a formal verification becomes practical, it is call "static checking" and then put into a tool like lint or valgrind.
Then, on the other hand, mindless use of such static checking itself can lead to severe bugs [1].
If not, isn't there any concern that (future) varified OS will render OBSD redundant one day?
No. Bernd [1] http://research.swtch.com/openssl
