Claiming "Fearless Concurrency" but ignoring synchronization bugs, at a low-level in concurrent data structures or at a high-level in concurrent systems is misleading. People will be fearlessly introducing livelocks.
And yes, writing that taught me that current programming languages are not sufficiently equipped to deal with concurrency bugs, including Rust. The bugs that I had where of the dining philosophers kind (deadlocks or livelocks when trying to put a thread to sleep for example or resolving data dependencies between multiple threads), some were due to a bug in glibc where only formal verification allowed me to ensure that I was doing the correct thing and it was the lower-level layers that was incorrect.[2]
Similarly, state machine formal verification to prevent design bugs is something that hardware engineers are deeply aware of but would also be extremely useful to ensure "correct-by-construction" event driven code in software engineering.
In comparison, we have many more tools to address memory bugs (Address Sanitizer, Valgrind and fuzzers in particular) but synchronization and communicating state machine bugs are still impractically addressed at the moment. This is something I'd really want Nim to explore and I'm really excited about the Z3 integration[3] to enable new formally verified use-cases[4].
Unfortunately, when I express concerns about those bugs to people from the Rust community, they tend to dismiss those as if the borrow checker was the panacea to all multithreading problems.
[1]: https://github.com/mratsim/weave
[2]: https://github.com/mratsim/weave/issues/56
> Similarly, state machine formal verification to prevent design bugs are something that hardware engineers are deeply aware of but would also be extremely useful to ensure "correct-by-construction" event driven code.
This reminds me a lot of P. Rust has a crate that I wouldn't necessarily recommend, but it might be similar to what you want:
https://github.com/fitzgen/state_machine_future
Of course, in this case the code is the model, there is no verification here.
The Z3 integration with Nim is super cool, would love to see something like that for Rust. I know of some existing research that reminds me of this but I don't have time to dig up the paper - it was implemented in macros, and looked a lot like what you've got there, with pre/post conditions, ensures, etc. If someone has that paper, please link it! I would love to reread.
edit: Here's one rust crate leveraging Z3, but not the one I was thinking of https://github.com/Rust-Proof/rustproof
