[karlding]

I'm curious if there's research into "better" primitives in Programming Languages in order to simplify writing distributed systems, analogous to how concurrency primitives beyond Mutexes, Semaphores, and Condition Variables (like Futures, Monitors, etc. or approaches such as Actors) can greatly simplify logic and enhance one's ability to reason about code. Or things like the Rust borrow checker.

The closest thing I'm aware of is TLA+.

[aphyr]

There's a lot of research into this, actually! Folks have been working on ways to extract executable code from Alloy, TLA+, Isabelle/HoL, and Coq specifications. That doesn't help with implementations which don't use codegen though--and it doesn't help you with the parts of the program that aren't formalized.

[jnwatson]

There are two general issues here: there's the nuts and bolts, and then there's the emergent properties of the protocol.

In my experience, async (which includes futures/promises, and actor-like mechanisms) makes the nut-and-bolts problems of avoiding variable race conditions, avoiding deadlock, managing multiple things going on, way easier.

You still need fuzzing and model checking to make sure you got the strategic stuff right.

That said, the team I work on is about to release our first Raft-based product, so I might have a different opinion in a few months.