Ironically, 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.
This 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.)
A 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.
