Hacker News new | ask | show | jobs
by maxbond 890 days ago
Rust comes to mind.
1 comments

How would Rust solve this problem?
All I meant was that it "proves semantic invariants in multi-threaded code," which proves the concept.
No data races is just a very tiny subset of semantic invariants, though.
I assumed what the poster above meant was that Rust can take care of more than just data races. Specifically Rust can solve the ABA problem somehow?
Rust won't solve the ABA problem, no. You'd be in unsafe Rust if you were writing something that could encounter the ABA problem.

You wondered out loud how it was even possible to do that kind of analysis, and that's where my mind went. Evidently people think it's a bad take. That's as deep as it goes.

The ABA problem is a false-positive execution of a CAS speculation on a shared memory location.

It is very easy to create an ABA problem in safe Rust. Data race free sequential consistency, which Rust has, is almost completely orthogonal to the ABA problem.

This is an area of active PLT research, we haven't come anywhere close to addressing the problem in the general case.

I suspect we'll be seeing all kinds of bugs caused by a generation of programmers thinking everything has guard rails in Rust because "safety", so they can turn their brain off and not think. In reality, those promises of safety largely disappear when threads, files, signals, and networks are involved.

At the end of the day, your programs run on computers which exist in the physical world. The abstractions are mostly isomorphic, but it's at the margins where the abstractions aren't isomorphic that all the interesting things happen.