Agreed. I just want to make clear that Rust/Ada/etc. don't give correctness guarantees! Their compiler is just more enforcing. It's all not black and white.

Rust is promoted for its correctness, but those correctness related bugs Rust prevents are an extremely low fraction of real world bugs (comparing to managed memory languages). I mean, how many type-system related bugs are there in real world projects with Java, C# or Go?

Rust is promoted with "fearless concurrency". Does it prevent your code from deadlocks, which are among the most tricky bugs?