Hmm. Maybe I don't understand what you're getting at here. It seems like you're suggesting something like a[b] = x could race in safe Rust because we don't know b in advance and maybe it ends up being the same in two threads ?

But Rust's borrow checker won't allow both threads to have the same mutable array a so this is ruled out. You're going to have to either give them immutable references to a, which then can't be modified and so there's no data race, or else they need different arrays.

This is boringly easy to get right in theory, Rust just has to do a lot of work to make it usable while still delivering excellent runtime performance.

Well, you could always require the programmer to supply a proof that the program is gonna be fine, before you compile anything.

(That means your programming language won't be Turing complete, but you can still code up anything you want in practice. Including Turing machines.)

The likes of Agda and Coq work in this way.