News for hackers. Stuff that matters.
Re:How the Boeing 737 Max disaster looks to a software Devel... by umvi on Thursday April 18, 2019 @05:14PM (#19694846)
Even then it doesn't matter if your software is "correct" if you don't understand/have not captured all the requirements.

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.

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.
Re:How the Boeing 737 Max disaster looks to a software Devel... by no-s on Friday April 19, 2019 @11:56AM (#19700564)
So true. The problem is in the system at a higher level. It is not really a software defect that killed all those folks.