It does not though? How does Rust proves that your implementation of a Peterson's lock algorithm[1] or Lamport's Bakery algorithm[2] is: - Deadlock-free - Liv

It does not though? How does Rust proves that your implementation of a Peterson's lock algorithm[1] or Lamport's Bakery algorithm[2] is: - Deadlock-free - Live-lock free - Free of data races Second, how does Rust proves that you are correctly using the relaxed, acquire and release atomics so that your channel implementation is free of data races? You can use Loom[3] but this is guarantee is certainly not provided by the compiler. In short, Rust compiler only addresses memory issues by flat out preventing memory sharing. However, someone has to write those sharing/synchronizing data structures (Channels, Event Bus, Concurrent Hash-Table, ...) and those people have no tools that help them navigate the significant complexity of multithreading that go beyond memory and lifetime bugs. [1]: https://en.wikipedia.org/wiki/Peterson%27s_algorithm#The_algorithm https://en.wikipedia.org/wiki/Peterson%27s_algorithm#The_alg... [2]: https://en.wikipedia.org/wiki/Lamport%27s_bakery_algorithm https://en.wikipedia.org/wiki/Lamport%27s_bakery_algorithm [3]: https://github.com/tokio-rs/loom https://github.com/tokio-rs/loom