Hacker News Reader

Comment by sansnomme | Hacker News Reader

There are tons of math majors produced every year. Would be a viable business model to offer factory-style program-correctness-proving-as-a-service. Current proof services are mostly niche static analysis for stuff like Ethereum contracts and occasionally a wannabe legal-tech company. I think aerospace could use more proofs. You can't use Ada for everything, eventually you will have to code in C/C++.

View on HN

As far as I have been able to gather, the MCAS software performed exactly to spec. You may have been drawn to the Boeing straw man narrative "the software was faulty (we can fix it)".

Algorithmic correctness won't necessarily help you if the root problem is bad sensor data.

Everyone knows what bad sensor data is until they have to write software to identify it.

That said, the way Boeing designed the MCAS is inexcusable. They actually had two sensors available, plus a full suite of other instruments and pilot inputs to cross reference and their solution is to only pay attention to a single sensor.

It was engineered like it was version 0.1 beta. When you realize that the -MAX crashes were very close to single fault accidents it's even more crazy. Normally to crash an airplane you need to thread the needle through multiple failure states thanks to redundancy and safe design. Simple single issue crashes are almost unheard of in the modern era thanks to decades of safety engineering. Aggressive cost engineering is returning us to the perilous air travel of the 40s and 50s.

Proof of correctness would be nice, but it looks like they failed at fault tree analysis or FMEA - both of which are common in aerospace.

Reply on news.ycombinator.com