It's still there. It's just a compile-time "race checker", not runtime.
It's still there. It's just a compile-time "race checker", not runtime.
Since in Rust it is illegal for a value to be referenced for writing in one place and referenced for anything else in any other place, regardless of concurrency/parallelism, Rust code is data-race free by design.
I still think that GP's comment was a non-sequitur.
Go's race detection says (with a high probability) you do or do not have any data races in the paths actually taken during some execution of your program. It is a (probabilistic) guarantee about how you ran your program.
Do you have some links about the known soundness issues? I was under the impression that although it hadn't yet been proven it was still a medium-term goal, and any soundness bugs were considered fairly major.
(And yeah, "mathematical proof" is strong regardless since e.g. LLVM is also in there somewhere. But it captures the idea more closely than any comparison of "compile vs. runtime" or "static vs. dynamic" does.)