> "Rust improves upon this situation by panicking in debug mode and wrapping in release mode, which is better than the Ada behavior in every possible"
So... What you're trying to tell us is that Ada recognising an exceptional situation has occurred is bad, and that Rust just ignoring it is a good thing? Righto... An integer overflow occurring in this scenario is an exceptional condition. In this case it was one that the developers did not anticipate. This issue arose because they mistakenly thought it was not possible for this scenario to occur. The mistake here was not anticipating the exception and handling it in a meaningful way, not the raising of an exception. The fact that not raising an exception would have avoided the disaster in this case is entirely incidental. It was still an exceptional circumstance that the developers, testers, designers did not anticipate. The silent wrapping behaviour you describe would have bitten someone eventually, perhaps here, perhaps somewhere else. Possibly with enormous repercussions.
> "Normal "unsafe" languages improve this by giving an incorrect value as the result, which in the case of Ariane V would have saved the flight."
The normal "unsafe" languages you're referring to ( presumably C ) have a history of very poor error handling. Requiring an extremely high degree of conscientiousness when programming for mission-critical applications. Can you imagine actually programming for what you're describing here? Not only does the computer have to guard against outright failure, but now it has to infer the possibility of an error state from a stream of in-band data in real-time. Righto...
Also, just so you know: Signed integer overflow is UNDEFINED BEHAVIOUR in C.
Probably the fact that the engineers got the case analysis wrong suggests that the methods of reasoning they were using weren't very effective. Modern formal methods might or might not have helped; guaranteeing that a piece of code is statically free of exceptions is not a terribly advanced thing to do, but really you'd like to guarantee that the variable was actually big enough. Having less code to reason about certainly would have helped.
C’s choice is clearly unconscionable.
I don't think there's an open-and-shut case that error values are "preferred or beneficial" in general with respect to exception handling through nonlocal control-flow transfers; there are reasonable arguments on both sides, and it seems likely that both are viable options in most circumstances, and which is better depends on those circumstances. (For example, lazy evaluation or catastrophic consequences attached to software crashes would seem to me to weigh heavily on the side of using error values, while interactive REPL-style usage would seem to me to weigh on the side of nonlocal control flow, perhaps with Common-Lisp-style restarts.)
My point was narrower: in this particular case, using error values analogous to NaNs, rather than shutting down the SRI, would have saved the rocket, without posing the risk of using garbage data that C's semantics pose. In this particular case, they would have been better. It's possible that, in other cases, perhaps even in other places in the SRI firmware, using error values would have been worse than unwinding the stack or shutting down the SRI. But in this case they would have been better.
(If you aren't convinced of that narrow point, you should probably read the report from the Lions board of inquiry.)
In the general case, the Ada behavior of detecting and signaling numeric errors seems to be the only robust choice to me. The alternative could only be acceptable if it's proven that the algorithms fail safe in the presence of tainted data.
However, default-ignore vs. default-explode isn't a difference between handling errors with IEEE-754-qNaN-style dataflow-tainting and CLU-style nonlocal control flow transfers, as you seem to think. In either case, algorithms that need data that could not be computed successfully will fail to get that data; in either case, you can write the code to either propagate that failure or to attempt to recover from it somehow. In either case, you will not be able to control the spacecraft if you needed that data to control it. The difference I was mentioning, which is not generally applicable, is that in unusual cases like the Ariane 5 disaster, where the erroneous data shouldn't have been computed in the first place because it wasn't needed, qNaN-style error handling clearly results in safer behavior.
But, in general, real-time control is not a place where there exists a "robust choice" when your software is broken. If your jet engine control software or your antilock braking software is broken, you're likely to die, and no error handling strategy can prevent that, at least not at the level we're talking about. Biological systems manage this situation by having a melange of somewhat-independent control loops using different algorithms that are constantly fighting for control of the organism; while this does seem to produce systems that are more resilient than engineered systems, it's less efficient and enormously more difficult to develop or understand, and it's the opposite direction from the rigorous certainty you and I favor.
Rust tries to give you zero-cost abstractions where possible. Overflow checks aren't zero-cost, therefore they're disabled in release mode. Otherwise when safety can be done at zero-cost (at runtime) Rust will usually do that.
I agree with you though that the exception might have helped in many other situations, especially if a simulation catches it early on. I would still say from gut feeling that ADA makes the safer decision on average.
And of course the run-time checks can also be disabled for Ada of course, and usually are for release build.
> These runtime checks[1] are costly, both in terms of program size and execution time. It may be appropriate to remove them if we can statically ensure they aren't needed at runtime, in other words if we can prove that the condition tested for can never occur.
> This is where the analysis done by GNATprove comes in. It can be used to demonstrate statically that none of these errors can ever occur at runtime. Specifically, GNATprove logically interprets the meaning of every instruction in the program. Using this interpretation, GNATprove generates a logical formula called a verification condition for each check that would otherwise be required by the Ada (and hence SPARK) language.
[1] overflow check, index check, range check, divide by zero
---
So again, I do not see why Rust would shine (as some people suggested) here, Ada/SPARK can statically ensure that your program is correct and eliminate all sorts of runtime errors, including overflow.
When I learned Ada (blog post somewhere in this thread) I was pretty shocked by how many more runtime checks it had than Rust does, overall. Rust usually checks things at compile time.
That's perhaps an oversimplification; elsewhere it's been said of Ada's mentality that "Incorrect Is Simply Not Allowed." — but there's ALWAYS been a preference for pushing checks from dynamic to static, and from runtime to compile-time.
As a trivial example, the following code is typically generated without any sort of index check because the loop-control variable takes its range from the Array, it's obvious that it CANNOT be an invalid index, and this is allowed by the language reference manual (and encouraged by the annotated reference manual)—
For Index in Input'Range loop
Input(Index):= 0; -- Zero the array.
End loop;
Value : Positive := Positive'Value( Get_Line );Also Ada does have wrapping arithmetic available. It just isn't the default.
This is not entirely correct. The code which overflowed was unnecessary for flight. People have this idea that the sensor sensed it was going 32745 m/s to the east one moment, and -32723 m/s the next, and then tried to compensate for the sudden gust of wind it must have encountered. This is incorrect. The routine in question was only supposed to run when it was on the ground, and served no purpose in flight. It was scheduled to be disabled 40 seconds after launch. (The flight failed after 37 seconds)
The problem is specifically the fact that the code was written in Ada. Ada does not fail the way other languages fail when you overflow. Instead of given an incorrect value (which never would have impacted the flight) it throws an exception. This exception was uncaught. This uncaught exception brought down the entire flight control system, despite the fact that the falling code was not controlling flight.
Rust improves upon this situation by panicking in debug mode and wrapping in release mode, which is better than the Ada behavior in every possible way. Normal "unsafe" languages improve this by giving an incorrect value as the result, which in the case of Ariane V would have saved the flight.