Re: Alleged "microkernel mathematically proven to be bug free"

I have a rough outline for a "cloud computing grid" that verifiably:

verifiably? _really_ provable stuff is a very scarce resource IMHO (especially in crypto. do you need crypto? Do you need P \ne NP?).

But it absolutely requires a verified microkernel. I'm *very *excited to see that we're making progress towards it.

Is it really a progress? There are assumption free proofs of False in most formal proof systems. Design flaws like \lor instead of \land pass the verification process and later are considered design flaws, not bugs in proof IMHO. Knuth quote: "Beware of bugs in the above code; I have only proved it correct, not tried it."