News for hackers. Stuff that matters.

A comment on How the Boeing 737 Max disaster looks to a software Developer. Parent comment

Re:How the Boeing 737 Max disaster looks to a software Devel... by AnimalMuppet on Thursday April 18, 2019 @06:29PM (#19695360)
> Bugs can arise where programs intersect in the real world.

Well, the context is flight control software for airplanes. If that code is bug-free but doesn't intersect the real world, that's rather useless. And if it intersects the real world but therefore is not bug-free, that's not a great argument for proofs of formal correctness.

But all of that is kind of beside the point. The MCAS specification was the wrong thing. Proving the implementation correct is useless. (You asked what is a bug in a spec? MCAS shows you the answer. Only taking input from one sensor is the wrong thing. Repeatedly applying nose-down is the wrong thing. It seems like I'm missing one or two more.)

[ Parent | on HN ]
Re:How the Boeing 737 Max disaster looks to a software Devel... by crimsonalucard on Friday April 19, 2019 @12:12AM (#19697044)
You can prove the code correct against the spec. However you can't prove that the spec will do what you expect it to do because the spec is where the intersection with the real world occurs. Therefore, you must test the spec. Everything that falls under the spec can be formally verified to 100% correctness.
[ Parent | on HN ]