3 ms·
> In other words, is it a genuinely simpler algorithm that provides the the same guarantees as Paxos, or is it simpler because it leaves edge cases unspecified,
by jberryman 12y ago
> In other words, is it a genuinely simpler algorithm that provides the the same guarantees as Paxos, or is it simpler because it leaves edge cases unspecified, forcing implementors to grind through the edge cases with heuristics?
Isn't it formally proven correct? And "simpler" would be subjective right? So what do you mean by "proven to truly be simpler than Paxos"? Thanks, and also that talk looks really great.
- tedsuo 12y agoI don't believe it has been formally proven correct. I would love to see evidence that it has been proven to be mathematically equivalent to Paxos.
- justinsb 12y agoMy understanding is that Raft has been proven formally correct in one of the author's PhD: https://ramcloud.stanford.edu/~ongaro/thesis.pdf https://ramcloud.stanford.edu/~ongaro/thesis.pdf (Chapter 8)
- alexnewman 12y agonaw dog, they got tla+ and shiznick
- tedsuo 12y agoThat's great, they hadn't done this when I last talked to them.