3 ms·

The trouble with formal proofs is that you can only prove that the code does what you say it does, not that it does what it needs to do. MCAS performed as desi

The trouble with formal proofs is that you can only prove that the code does what you say it does, not that it does what it needs to do. 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.

tluyben2 8y ago
Yes, agreed, but for life or death situations, as a programmer, I would prefer to use all tools at our disposal; besides money it does probably improve the quality if you spend this time.
- mikeash 8y ago
  I think this is likely to be true, but I do wonder if there might be a better way to spend those resources. For this particular example, you’d have been better off putting more money into flight testing with various sensor errors.
  - tluyben2 8y ago
    Well, yes. But, and who knows if it is true, but you would think you can think up that you need sensor errors to be tested and maybe figure out you need three errors vs two for instance to cover all cases; formal systems can help you model and reason about that and come up with cases that are not covered. 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.
    - mikeash 8y ago
      Two sensors is enough if you can shut off the system when they disagree. MCAS didn’t doom the plane if it shut off, so that was enough. The problem was that they didn’t do this, and instead used only one sensor at a time. Basic sense and standard practice tells you not to do that. I don’t know if more formality would have helped them not do something so boneheaded. 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.

tluyben2 8y ago

Yes, agreed, but for life or death situations, as a programmer, I would prefer to use all tools at our disposal; besides money it does probably improve the quality if you spend this time.

mikeash 8y ago
I think this is likely to be true, but I do wonder if there might be a better way to spend those resources. For this particular example, you’d have been better off putting more money into flight testing with various sensor errors.
- tluyben2 8y ago
  Well, yes. But, and who knows if it is true, but you would think you can think up that you need sensor errors to be tested and maybe figure out you need three errors vs two for instance to cover all cases; formal systems can help you model and reason about that and come up with cases that are not covered. 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.
  - mikeash 8y ago
    Two sensors is enough if you can shut off the system when they disagree. MCAS didn’t doom the plane if it shut off, so that was enough. The problem was that they didn’t do this, and instead used only one sensor at a time. Basic sense and standard practice tells you not to do that. I don’t know if more formality would have helped them not do something so boneheaded. 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.