7 ms·

That seems pretty accurate, TBH. Correct distributed consensus is almost exclusively done via some flavor of Paxos. As for the actual research, it probably ne

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.

m0zg 5y 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.
ncmncm 5y 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.
- Jweb_Guru 5y 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/ https://emptysqua.re/blog/paxos-vs-raft/.
  - ncmncm 5y ago
    ...which is what I just said: the proof is about Paxos, not Raft, and so applies to relatively rarebsystems that do rely directly
    - ncmncm 5y ago
      [Buggy HN.] ... relatively rare systems that do rely directly on Paxos, not Raft.
      - Jweb_Guru 5y 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).
        ncmncm 5y 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.
- deleted 5y ago
  [deleted]

m0zg 5y 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.

ncmncm 5y 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.

Jweb_Guru 5y 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/ https://emptysqua.re/blog/paxos-vs-raft/.
- ncmncm 5y ago
  ...which is what I just said: the proof is about Paxos, not Raft, and so applies to relatively rarebsystems that do rely directly
  - ncmncm 5y ago
    [Buggy HN.] ... relatively rare systems that do rely directly on Paxos, not Raft.
    - Jweb_Guru 5y 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).
      - ncmncm 5y 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.
deleted 5y ago
[deleted]