paxi

Author seems to be using https://github.com/ailidani/paxi for actual implementation and proof. I'm more of a python/rust guy. There have been some attempts to make model checkers in rust: https://github.com/stateright/stateright The issue is that rust is a very large language and it's hard to get it right. I have a python implementation of raft over here: https://github.com/adsharma/raft/tree/master/raft/states That's small enough to be self contained and perhaps run through a model checker some day and transpiled to many statically typed languages. The issue with TLA+ proofs such as: https://github.com/fpaxos/raft.tla is that it's hard to tell if a particular C++ or Rust implementation conforms to the spec. So how do we check and transpile? * https://www.philipzucker.com/Modelling_TLA_in_z3py/ * https://github.com/adsharma/py2many

This is something I've noticed recently -- more and more researchers are starting to write reference implementation code for networking and distributed systems in Golang. In my own head, it makes sense -- golang is simple to read if not verbose, doesn't require crazy formatting, has excellent standard library support, and has relatively painless concurrency, and can be run as a scripting language. No it's not as easy to get started with as Python, Ruby or Perl, but only one of those has easy-to-spawn native threads, nevermind lightweight coroutines (and the one with native threads encourages illegible code). If you're not doing type theory work or very specific exploration in a specific field, I don't know another language that is so easy to get up and running with. On top of all this go's performance is pretty great/consistent as well, J