4 ms·
1) and 3) are related as far as I remember - Ada WOULD have found the problem which was responsible for the Ariane 5 launch failure, but the section involved wa
by sgift 10y ago
1) and 3) are related as far as I remember - Ada WOULD have found the problem which was responsible for the Ariane 5 launch failure, but the section involved was speed critical, so the asserts were dropped to make the code run fast enough.
Sad reality: The best security features in the world are useless if they are too slow for your use case.
- rcxdude 10y agoIronically, it's also Ada's asserts which contributed to the failure (though far from the root cause): The result of the erroneous calculation wasn't actually used, so just ignoring it like C would have would have been fine. It was the fact that the wrong cast caused the software to abort which resulted in the crash.
- AstralStorm 10y agoThis is why static checking is better than runtime checking. Rust has some, but not enough. What is needed is something like Isabelle sledgehammer, quickcheck and metis logic and higher function correctness checkers. (Yes, Haskell has a bit more primitive version of Quickcheck.)
- kqr 10y agoThat's basically what SPARK Ada is.
- AstralStorm 10y agoA smaller less featured one, but very useful nonetheless. (Specifically, sledgehammer is superior as a checker and automated proof library check is also invaluable in simplification.) Technically, Why3 (intermediate language and prover manager used in SPARK for verification) can interface with Isabelle too. I should try it out. More edit: someone has done it, called HOL-SPARK. Excellent.
- SAI_Peregrinus 10y agoA Denial of Service vulnerability is a security vulnerability no matter the cause. That COULD be an attacker, but it could also be that your code runs too slowly or the UI is too hard to learn.
- efalis 10y agoIt was actually an engineering error. The software in question was designed for Ariane 4, and the condition that happened in Ariane 5 could not occur. But a shortcut was taken, and the suitability of the software was not reassessed. Then Ada's exception mechanism was pulled into play when it never should have been given the requirements of the Ariane 4.