Earlier quoted context omitted.
I'm not sure you understand how difficult it is to prove software correct. I've written a decent amount of Coq code. It's quite bonkers how much of proof one needs to write to get anything done. For reference, the certified compiler CompCert's code base is something like 10% code and 90% proofs.
No, I get it, but still... it's ironic. Software for a plane, though, I would want 1% code 99% proofs.
> The fly-by-wire flight software for the Saab Gripen (a lightweight fighter) went a step further. It disallowed both subroutine calls and backward branches, except for the one at the bottom of the main loop. Control flow went forward only. Sometimes one piece of code had to leave a note for a later piece telling it what to do, but this worked out well for testing: all data was allocated statically, and monitoring those variables gave a clear picture of most everything the software was doing. The software did only the bare essentials, and of course, they were serious about thorough ground testing.
> No bug has ever been found in the “released for flight” versions of that code.
so not quite that tests are useless because blackbox, but more that yes, it is possible to write software that facilitates showing a code will do what it says it will do.
In another note, I do feel sorry for the engineers but at the same time Airbus also has similar MCAS system, but the only thing that saves them is an extra Angle-of-Attack sensor whereas I believe the boeing relied on just one or two. Airbus had 3 AOA sensors and if 2 agreed, that was the data fed into the MCAS.
It still boggles my mind that they would place a bigger engine when the original plane was not built for it at all, this was 100% profit orientated move to prevent Airbus from taking Boeing's majority marketshare, it's highly ironic that the opposite results.
Even more infuriating is that Boeing passed it off as the exact same plane, not much extra training is necessary, along with FAA giving their blessing, now caught up in the mess.
Canada for instance is now looking to the EU for an independent auditing, as any credibility FAA has built up over the past years has taken a significant hit.