Paxos vs. Raft: Have we reached consensus on distributed consensus?

I think the difference in our stances arises from the two ways in which the term 'Paxos' is used. In the part-time-parliament paper, the single-decree paxos is the fundamental building block. I'm assuming this is what you think of as Paxos, and you are right in your assertion. It is defined as the fundamental act of consensus.

However, I have always viewed the single-decree protocol as a pedagogical device; a single write-once distributed register is useless in practice, so the multi-decree protocol is where it becomes useful, and to me is the point of the paper. I say this for a few reasons: a) state machine replication has been Lamport's focus since his early papers, including the 'time clocks and ordering' paper. (b) in engineering-oriented papers such as 'paxos made live', 'chubby' and so on, the term is used as a proxy for a replicated log. The reason for the many variants of Paxos is due to the underlying impulse that basic paxos is not sufficient in and of itself. You need some variant of shared log or equivalently, atomic broadcast.

So, we are both right in our ways. We can have consensus, as long as we sacrifice consistency of the definition of 'Paxos' :)

I used to follow Jepsen https://jepsen.io/ closely. Those tests are quite comprehensive. But I think even those are not sufficient to quantify the quality of Paxos/Raft.

Tools like TLA+ probably require a few months to learn and become proficient.

If you feel confident you've built a complex algorithm like this correctly on the first try you probably haven't. Hubris and distributed systems just don't mix.

Verifying correctness to back up our empirical claims is often the hardest and most overlooked part of software engineering.

This is a proportionate response to an undergraduate trying to sell you his new RDBMS. But most students really did write a b-tree. Academic programming elides the supporting infrastructure that bridges the gap between algorithm and software system. Textbooks aren't generally leaving out 100 pages of extra steps required for the list to actually be sorted or the path to actually be shortest. And so a student is not exactly out of line for thinking that the Raft he was taught is actually consistent in the presence of failure. I'll defer to the community's wisdom that he's wrong! But he's still not out of line.

If anything, I'm worried about these classes instilling false confidence. People who think they know these algorithms may go implement them professionally, and not have anyone around to tell them the full story. Cryptography education is careful to put asterisks around "Textbook RSA." Distributed systems education should probably be doing the same.

this is almost independent with how hard is to build a (good) pure implementation of raft that offers a simpler API