5 ms·
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 pro
by sansnomme 7y ago
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++.
- jandrese 7y agoAlgorithmic correctness won't necessarily help you if the root problem is bad sensor data.
- Gibbon1 7y agoEveryone knows what bad sensor data is until they have to write software to identify it.
- jandrese 7y agoThat 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.
- deleted 7y ago[deleted]
- clon 7y agoAs 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)".
- phkahler 7y agoProof of correctness would be nice, but it looks like they failed at fault tree analysis or FMEA - both of which are common in aerospace.