2 ms·
I actually think far more of these safety of life standards should require formal proof. IMNSHO the standards were set so low so that C++ could clamber over th
by tialaramex 2y ago
I actually think far more of these safety of life standards should require formal proof.
IMNSHO the standards were set so low so that C++ could clamber over the low bar, and it's a happy consequence in some sense that Rust has no trouble clearing it, but the bar should be raised considerably instead. Software crucial to the safe operation of an airliner ought to be proven correct, not just slapped together in any of the general purpose languages, including Rust and then subject to a bit more process than for a web app.
- adrianN 2y agoThat would explode the costs for marginal safety improvements. I think the same effort spent on better requirement engineering would yield more payoff.
- tialaramex 2y agoWhy do you believe this would "explode the costs" ? Why would the resulting safety improvements be "marginal" ?
- adrianN 2y agoBecause proving correctness for complex software is difficult and very few people have relevant experience. So it is both labor intensive and you need to pay high wages. I believe the safety improvements are marginal because of my experience in safety critical development. Almost all the bugs we did not find by testing turned out to be problems with the requirements that led to interoperability issues. Proving the correct implementation of wrong requirements would not have helped.