[belter]

I talked about Software based solutions that is also why I referred to summation/consensus based systems like the Shuttle had. I even believe they used different programming languages, since of course compilers can also have bugs.

To use an example like seL4, is formally proven correct against its specification. But how we got the specification itself correct?

"Hidden Fallacies In Formally Verified Systems" https://smartech.gatech.edu/bitstream/handle/1853/62855/BOBE...

How seL4 or CompCert protect me against against hardware issues like ECC errors, or the Pentium FDIV ? [1]

To humbly quote Knuth:

"Beware of bugs in the above code; I have only proved it correct, not tried it."

[1] https://en.wikipedia.org/wiki/Pentium_FDIV_bug

[jnash]

It is a lot easier to get the spec right than getting the implementation right.

> How seL4 or CompCert protect me against against hardware issues like ECC errors, or the Pentium FDIV ?

That's a straw man argument. Nobody claims that formal proofs can protect you from hardware failures. However formal proofs can protect you against Pentium FDIV style bugs (see ARM formal specification efforts). Intel started massively investing in formal proof methods because of the not-formally-proven-correct Pentium FDIV fiasco.

[belter]

Thanks for replying, but I insisted in my previous post that I referred to Systems and Solutions.

In real world use, and other than in academic contexts, is of reduced usefulness that I claim my component used TDD and was formally verified, while throwing over the wall, the responsibility of delivery for a system that can't fail, to somebody else.

So my claim is, we don't know how to do it, we can formally verify some components, and we hope the spec is correct.

Forgetting the spec only has the known known's and unknown known's, but not the unknown unknowns, is a kind of intellectual hubris I am not willing to bet lives on. Certainly not under the disguise of using formal methods.

So I am referring to examples like this:

"A380 Flight Controls overview" [1]

• 3 PRIMary Flight Control and Guidance Computers integration of Auto Flight (ex FGEC) and Flight Control (ex FCPC)

• 3 Auto-Pilots

• 3 SECondary Flight Control Computers dissimilar Software and Hardware, simpler Control Laws

[1] https://www.fzt.haw-hamburg.de/pers/Scholz/dglr/hh/text_2007...