[belter]

We are in the year 2022. We don't have the technology to produce bug free software based solutions.

100% code coverage, as other mentioned in this thread, does not guarantee you exercised 100% of all the inputs values possible.

That is why:

- You can pay millions of dollars to a Software Company, and when you install the product the usual license text, says something in capitals along the lines of: NO GUARANTEES WHATSOEVER FOR ANYTHING... plus some will mention you can't use for controlling X-Ray machines, Nuclear Power generators and so.

and also why

- Software where life depends on, normally will use a type of summation or consensus based software like the Shuttle had with 3/4 computers.

[marginalia_nu]

I don't think it's entirely technological limitation. More often than not, the discovery of bugs is increased understanding of what we require from the code. We often say a code is buggy when it surprises us in some fashion, then we tacitly invent a new requirement we say it has violated.

If you have a function

  F(signed int32 n) -> (signed int32 A, signed int32 B) 

that returns two integers (A, B) so that

  A*B = n

and we discover that F(2) -> (-2, 2147483647), which is entirely correct in a language that permits integer overflow; then we call it a bug because A and B must be smaller than n (or whatever). This was not a requirement until the bug was discovered.

[rmetzler]

I’m not really sure if this was understandable, but I’m basically in the same camp as you are.

It’s next to impossible to have 100% bug free code. Automatic testing helps and TDD helps to write tests, but it’s not the goal. The goal is to create code that is well tested and easy to change.

[jnash]

> We don't have the technology to produce bug free software based solutions.

Not correct. See seL4, CompCert etc.

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