Hacker News new | ask | show | jobs
by belter 1554 days ago
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...