[jt_thurs_82]

> the most foundational distributed computing protocols—known as Paxos—meets its specifications.

> Paxos is one of the most important examples of the category

>“Most—if not all—consensus algorithms fundamentally derive concepts from Paxos,” Goel said.

A lot of burying the lede here, trying to imply Paxos powers many more applications than it actually does. While Paxos is in decent widespread use, and influential, I find some of the verbiage here lying by omission.

[User23]

First, automatically checking Paxos is very cool. Nothing I'm saying in any way diminishes that achievement.

Next, the result is entirely unsurprising. Paxos is proved correct since its construction was formally derived[1] to be so.

Finally, this is a nice opportunity to highlight the distinction between program verification and program derivation. In general, it's considerably easier to derive a program that has a property than it is to verify that an arbitrary program has a property. For example the halting problem is uncomputable in general and yet it's easy for a competent programmer to derive loops that always terminate. This is analogous to how it's much easier to determine that some large number is the product of two primes when you yourself produced it by multiplying those same two primes than it is to factor the product when the multiplier and multiplicand are not already known.

[1] https://www.microsoft.com/en-us/research/uploads/prod/2016/1...

[Jweb_Guru]

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]

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]

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]

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/.

[ncmncm]

...which is what I just said: the proof is about Paxos, not Raft, and so applies to relatively rarebsystems that do rely directly

[ncmncm]

[Buggy HN.] ... relatively rare systems that do rely directly on Paxos, not Raft.

[Jweb_Guru]

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).