Hacker News new | ask | show | jobs
by Jweb_Guru 1690 days ago
That seems pretty accurate, TBH. Correct distributed consensus is almost exclusively done via some flavor of Paxos.

As for the actual research, it probably needs much closer reading, but if they can automatically infer nontrivial inductive invariants that's huge for automatic verification, since this is the usual stumbling block for those kinds of tools.
2 comments
m0zg 1690 days ago
Most people have never dealt with large resilient systems, and do not understand what "distributed consensus" even means, and what it enables. Hence the derisive comments on this important result.
link
ncmncm 1689 days ago
As I understand it, Raft is much more commonly relied upon than Paxos. Raft uses concepts from Paxos, but is not Paxos. So, a proof about Paxos is not a proof about Raft.
link
Jweb_Guru 1689 days ago
Raft is more or less a Paxos variant with good marketing. Sure, the proof for vanilla Paxos won't directly apply, but it's not inaccurate to say that it derives heavily from Paxos, which is all the quote above was saying. See https://emptysqua.re/blog/paxos-vs-raft/.
link
ncmncm 1689 days ago
...which is what I just said: the proof is about Paxos, not Raft, and so applies to relatively rarebsystems that do rely directly
link
ncmncm 1689 days ago
[Buggy HN.] ... relatively rare systems that do rely directly on Paxos, not Raft.
link
Jweb_Guru 1689 days ago
If you read the article, you can see that there are barely any material differences between Paxos and Raft. Certainly no more than there are between the description of a program as an abstract state machine and its actual implementation (and based on our other comment thread, you seem to be under the impression that there is not much difference there).
link
ncmncm 1689 days ago
I don't need to read the article to know that Paxos and Raft have substantial commonality. That does not make them the same. That does not make a proof about one a proof about the other. That does not make a program that implements one a program that implements the other.

An abstract state machine, such as defines a version of Paxos, maps trivially one-to-one to parts of a program that implements it. A different abstract state machine, such as one that implements Raft, maps trivially one-to-one to a different program.

You might reasonably demonstrate that two different state machines define the same system behavior, but you would need to provide that demonstration. That has not been reported.

link