Hi, this is my first post in /r/ada, so I hope I'm not breaking any etiquette. I've briefly dabbled in Ada many years ago (didn't try SPARK, sadly) but I'm currently mostly a Rust programmer.

Rust and Ada are the two current contenders for the title of being the "safest language" in the industry. Now, Rust has affine types and the borrow-checker, etc. Ada has constraint subtyping, SPARK, etc. so there are certainly differences. My intuition and experience with both leads me to believe that Rust and Ada don't actually have the same definition of "safe", but I can't put my finger on it.

Could someone (preferably someone with experience in both language) help me? In particular, I'd be very interested in seeing examples of specifications that can be implemented safely in Ada but not in Rust. I'm ok with any reasonable definition of safety.