> For any project where performance or correctness are significant concerns I'd much rather use Rust than Python. It provides a lot more tools to help you write correct code, and express invariants in a machine-checkable way. This means that they are maintained when the code changes, even when multiple contributors are involved. I'm must more confident in my ability to ship correct code in Rust and maintain that correctness over time.
Ada/Spark is more about mathematically proving that your program works. Rust is more about that your program won't trample memory and won't crash.
That said, Rust seems to have reasonably good performance compared to C/C++. Also the concept of lifetimes is interesting too.
Just because your program compiles in C++/Ada(no-spark)/C/Java/Rust doesn't mean it's correct. If it compiles in Rust, the compiler is telling you it's memory safe and thread safe.
If you have a lot of string handling the strictness and ease of safe zero copy in Rust would make it unbeatable for performance and safety.
Due to lifetimes it's easy to keep string slices as references into the original memory and if you do need to modify some strings, you can use CoW.
The way Rust deals with encoding also makes it much safer to use Rust. Since you need to be very explicit about which encoding you convert to what and if you want to allow lossy conversions.
I don't think there is much of an equivalent in ADA for this. ADA has other benefits, like the delta (fixed point) types which help a lot in embedded projects.
Any reason for why Rust over Ada/SPARK?