Comment by johnisgood

... and formal verification is where Ada / SPARK wins over Rust.

I mean, we can go on but I think it quite ends there, as far as safety goes. :D

There is a reason for why Ada is used in industries that are mission-critical.

> Ada needs a profile that guarantees that code can't be the source of erroneous execution and constrains bounded errors further.

Not really, you can just use Ada / SPARK and it is all checked at compile-time. Look for my comments where I mention Ada.