Hacker News Reader

Comment by morelisp | Hacker News Reader

Rust's compiler checks a mathematical proof that, if your types are valid (e.g. you didn't do anything bad during `unsafe`) you do not have any data races. It is a guarantee about your program per se.

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.

View on HN

It's not a mathematical proof in the literal sense (yet), because there are known soundness bugs in Rust that are yet to be addressed; moreover the interaction of borrow checking (including interior mutability) with the traits system is poorly understood and has not been proven to be correct even in a simplified model. It should yield a meaningful level of checking, and if nothing else, the ergonomics is way better than just running a static analysis on C/C++ code (setting aside the question of whether current static analysis tools can even check for possible data races); but you shouldn't rely on it to that extent.

I don't program Rust regularly or track its status in that much detail, so thanks for the correction.

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.)

https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao... is the list of soundness bugs. They are considered major, but they’re more compiler bugs than something broken in the language itself. They are taken seriously, but bugs will always happen. Some need upstream fixes, too, so that can take a while.

Reply on news.ycombinator.com