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.
MCAS performed as designed. Only reading one AoA sensor, acting on bad readings, not rejecting values that are clearly out of bounds, operating continuously without any limits on its pitch authority, all of this was how is was designed to work. You could have proved MCAS “correct” and ended up with the exact same result.
A lot of software problems are due to discrepancies between the design and the implementation, of course. But it’s not a panacea.
I think the point is which these disasters show, and some others in the past (was there not a recalled Japanese car with a software issue?) that a few million more for the right resources will save you a lot more down the line. Problem is that this is not really a statement we can prove for formal verification because we do not have enough to compare with; i have a very strong feeling it will make quite a significant difference; if not for the proofs themselves then for the sheer number of hours and time the proofwriters thought about it by the time of delivery.
However, this looks like an unusual case. Based on the fact that they had such a dumb design for this system, that shouldn’t have passed muster in any aviation context no matter your software methodology, it’s probably not representative enough to draw a larger lesson about engineering. The larger lesson seems to be business and regulatory.
Regarding Japanese cars, Toyota went through a big thing with unintended acceleration that got quite a few people killed. Software was suspected, but the cause was ultimately determined to (mostly?) be a combination of drivers mixing up the accelerator and the brake (happens more often than you might think) and unsecured floor mats pushing the accelerator down. I bought a Toyota not too long after this and the dealer made a special point to show me how the floor mat attached to the floor and that I must be sure it was solidly connected.
Their software was audited and apparently it was really badly made. It was described as “spaghetti-like” and had global variable abuse, ignored errors, failed to restart unresponsive tasks, and had potential memory corruption problems. It’s quite possible that this really was the cause, and a jury even found this to be the cause in a civil trial over one of the crashes, but it was never definitely linked.
How do you solve it? Assume your AoA sensor is always correct? Congratulations, MCAS is a provably correct solution! Make the sensor behavior more complex? Sorry, the problem is now intractably complex (and still doesn't model the actual hardware).
A necessary part of why types are so useful is that understanding the types is easier than understanding the code itself.
If the types become so complex that they start to get harder to understand than reading your code (e.g. C++ template errors can sometimes get this bad), then they are no longer helpful.
> 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.
Note however that there were several software-related crashes in the early days of Gripen. Might not be related to exactly this code, but to the problem of regulating the feedback loops to manage the plane's purposeful instability
Off topic but here's a neat youtube video of Gripen jets undergoing rapid turn-around, on a normal street road with just a handful of people, and special tools for the crew:
Second crash (over middle of Stockholm) https://youtu.be/mkgShfxTzmo?t=133
From Wikipedia: During the test programme, concern surfaced about the aircraft's avionics, specifically the fly-by-wire flight control system (FCS), and the relaxed stability design. On 2 February 1989, this issue led to the crash of the prototype during an attempted landing at Linköping; the test pilot Lars Rådeström walked away with a broken elbow. The cause of the crash was identified as pilot-induced oscillation, caused by problems with the FCS's pitch-control routine.[22][33][34]
In response to the crash Saab and US firm Calspan introduced software modifications to the aircraft. A modified Lockheed NT-33A was used to test these improvements, which allowed flight testing to resume 15 months after the accident. On 8 August 1993, production aircraft 39102 was destroyed in an accident during an aerial display in Stockholm. Test pilot Rådeström lost control of the aircraft during a roll at low altitude when the aircraft stalled, forcing him to eject. Saab later found the problem was high amplification of the pilot's quick and significant stick command inputs. The ensuing investigation and flaw correction delayed test flying by several months, resuming in December 1993.[22]
the second was even more shocking, all of a sudden it looked like he was trying a Cobra maneuver until he ejected! that's insane.
That's extremely different to a system that silently severely mistrims you, then tells you to disable your ability to trim electrically before you can fix the mistrim, as if that even makes sense, all while overpowering the yoke with aerodynamic load.
For the record, Airbus's three sensors haven't prevented crashes completely. Here's one where two sensors were damaged, causing the correct sensor to be treated as erroneous and lose the quorum vote:
https://en.wikipedia.org/wiki/XL_Airways_Germany_Flight_888T
I like really long function bodys so I get turned on by the idea.