4 ms·
I'm truly glad that you're enjoying that paper :) This is completely unrelated, but I found this paper to be similarly brilliant in its simplicity, clarity, an
by omginternets 11y ago
I'm truly glad that you're enjoying that paper :)
This is completely unrelated, but I found this paper to be similarly brilliant in its simplicity, clarity, and rigorous explanation: https://ramcloud.stanford.edu/raft.pdf https://ramcloud.stanford.edu/raft.pdf
- zeckalpha 11y agoThat paper took 25 years to refine. Additionally, for the right audience, more math could make it more succinct.
- omginternets 11y agoI don't doubt it, but I'm not sure what you're trying to say. Would you elaborate?
- catnaroek 11y agoI have a hard time already convincing myself that correct sequential imperative algorithms are indeed correct - which probably means that I'm a bad programmer, but I can't change who I am. So convincing myself that that Raft, a concurrent algorithm, is correct (meets its specification) from an informal description is completely out of question - where is the formal proof of correctness?
- mbrock 11y agoTake a look here for pointers to formal proofs: https://news.ycombinator.com/item?id=10017549 https://news.ycombinator.com/item?id=10017549 Specifically Verdi, a Coq framework for distributed system verification, which now includes a formally proven Raft implementation. https://github.com/uwplse/verdi https://github.com/uwplse/verdi This appears to be the main theorem, "raft_linearizable": https://github.com/uwplse/verdi/blob/master/raft-proofs/EndToEndLinearizability.v https://github.com/uwplse/verdi/blob/master/raft-proofs/EndT...
- catnaroek 11y agoThank you very much. :-)
- omginternets 11y agoAh, sorry. I think you're reading this with a much deeper understanding of mathematics than I. I'm really curious, though. Could you give me some insight into how algorithms are proven correct?