Personally, I'm surprised that the majority of the HN community overlooks or ignores the reports from NASA and Exponent (Toyota's outside expert witness) in favor of the testimony from Barr, the witness for the plaintiffs in the Oklahoma case. (I'm honestly amazed that Barr was allowed as an expert witness) Barr did show that the code "smelled" and that it was possible to inject specific faults to induce an uncommanded acceleration, but he did not show that his proposed failure mode occurred nor that it was probable to occur. In fact, part of his failure mode was that it left no record of a DTC. It's the perfect kind of failure mode for a sympathetic plaintiff to wield against an arrogant defendant with deep pockets: possible that it occurred, possible to demonstrate, understandable for a jury (who hasn't had a BSOD?), and impossible to disprove.
You bring up the practice of software engineering, but I think you need to place it in context of how software engineering was practiced around the time that the electronic throttle system was developed. MISRA, which HN readers are becoming aware of, didn't exist. Proof assistants, which today remain challenging to use and integrate into an SLDC, were even more arcane. In fact, your example of TLA+ wouldn't fly even today since TLA+ doesn't do code generation, and that would be a necessary component of the verification process of a regulated SLDC. I don't think TLA+ existed at the time either. Things certainly have changed!
