I don't see the point with "zero-cost abstractions", overflow check is not an abstraction.
And of course the run-time checks can also be disabled for Ada of course, and usually are for release build.
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 );