Hm, so can Ada/SPARK bring the same memory safety/data race guarantees to the table as Rust, yet not being more difficult to express and maintain those guarantees? I'm not familiar with the language.