This is a really good post. I liked seeing the TLA+ code here. There's a pretty serious ambiguity in the Paxos Made Simple paper, which makes it very easy to fo

This is a really good post. I liked seeing the TLA+ code here. There's a pretty serious ambiguity in the Paxos Made Simple paper, which makes it very easy to follow the paper and still end up with a broken algorithm. From Lamports publications page (https://lamport.azurewebsites.net/pubs/pubs.html#paxos-simple https://lamport.azurewebsites.net/pubs/pubs.html#paxos-simpl...): > In 2015, Michael Dearderuff of Amazon informed me that one sentence in this paper is ambiguous, and interpreting it the wrong way leads to an incorrect algorithm. Dearderuff found that a number of Paxos implementations on Github implemented this incorrect algorithm. Apparently, the implementors did not bother to read the precise description of the algorithm in [122]. I am not going to remove this ambiguity or reveal where it is. Prose is not the way to precisely describe algorithms. Do not try to implement the algorithm from this paper. Use [122] instead. Lamport's core point here is using something like TLA+ to describe algorithms like this is essential. Writing is just too prone to ambiguities and misunderstandings, and the formalism really helps. The downside, obviously, is that TLA+ can look impenetrable if you're not familiar with it. While it's not hard to learn (the mathematical underpinnings are quite simple), the initial curve is quite steep. It's not that simpler written descriptions are bad, just that it's hard to make them exact enough to communicate the algorithm perfectly. On the other hand, learning from the mathematical notation is pretty hard. I don't know how to fix this problem.