Re:How the Boeing 737 Max disaster looks to a software Devel...
by AnimalMuppet on Thursday April 18, 2019 @06:20PM
(#19695320)
This. MCAS was the wrong thing to build. The wrong thing, correctly built, is still wrong, no matter how perfect the formal verification.
You could write a formally verified MCAS system in Coq or whatever that still kills people because you didn't consider the case of sensor failure (because that wasn't in the requirements). Or because you didn't consider the case of double sensor failure or a combination of extremely rare hardware failures (that wasn't in the requirements either!).
Your code is mathematically perfect, yes! But it was built with the incorrect assumption that the hardware is perfect as well!
I'll take a robust set of tests written by someone thinking outside of the box in terms of what could fail, how it will be used in operation, etc. over a piece of software "guaranteed unsinkable" because it is formally verified.