Rust is much less expressive (meaning, it is not able to say many interesting things about the system) and far harder to reason about than the much simpler and

Rust is much less expressive (meaning, it is not able to say many interesting things about the system) and far harder to reason about than the much simpler and more expressive (though less familiar an un-compilable) TLA+. In fact, here[1] is some work by someone who designs concurrent/distributed algorithms in TLA+ and implements them in Rust. This is not a shortcoming of Rust in particular. No programming language can be as expressive and as simple as a specialized specification language like TLA+ (it could be by essentially embedding a specification language in some specification tier of the language -- like the type level in languages with dependent types like Idris or the contract level like languages with formal contracts like Java with JML or SPARK, but this comes at the cost of either less expressive power and/or much increased complexity) [1]: https://github.com/spacejam/tla-rust https://github.com/spacejam/tla-rust