Hacker News new | past | comments | ask | show | jobs | submit login

AFAIK, you still have to be very careful since data races based on data dependencies can never be excluded in general, that is theoretically not possible. What you get is a guarantee that your program is not in an undefined state. There are still plenty of ways to shoot yourself in the foot with incorrect synchronization.



> AFAIK, you still have to be very careful since data races based on data dependencies can never be excluded in general

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.


> AFAIK, you still have to be very careful since data races based on data dependencies can never be excluded in general, that is theoretically not possible.

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.




Consider applying for YC's Spring batch! Applications are open till Feb 11.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: