For those who have implemented 2 phase commit, 3 phase commit:
-
was Rust's type system useful in catching errors ?
-
did you use tla+ / other model checkers ? are any of them good for auto generating Rust code ?
EDIT: More generally, there is the question of: Rust's type system is great at helping prevent errors when we have multiple threads accessing the same memory.
However, is there a way to use / abuse the type system to help verify correctness of distributed algorithms. If so, how. If not, are there tools for verifying distributed algorithms that can also synthesize Rust code ?