[steveklabnik]

The rust compiler also removes bounds checks and such if it can statically prove that they won't occur. You don't have as much tooling to communicate it to the compiler as you do in SPARK just yet.

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.

[OneWingedShark]

>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;

Conversely, there are places where you cannot statically determine the validity:

    Value : Positive := Positive'Value( Get_Line );

[johnisgood]

More information about Get_Line: https://blog.adacore.com/formal-verification-of-legacy-code