3 ms·
Are they talking about computer verified proofs? I wonder, are researchers able to prove the correctness of distributed algorithms the same way they would prov
by yodsanklai 12y ago
Are they talking about computer verified proofs?
I wonder, are researchers able to prove the correctness of distributed algorithms the same way they would prove sequential algorithms (for instance, using some type of Hoare logic and sat solver/ proof assistant).
- mazieres 12y agoNo. At least for the moment, the proofs are English language only.
- djb_hackernews 12y agoYou may be interested in this[0] paper outlining AWS use of TLA+ to formally prove its systems. Also previous discussion here[1]. [0] http://research.microsoft.com/en-us/um/people/lamport/tla/formal-methods-amazon.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/fo... [1] https://news.ycombinator.com/item?id=8096185 https://news.ycombinator.com/item?id=8096185
- ziedaniel1 12y agoIf anyone's interested in proving distributed algorithms correct, they should check out the Verdi project (https://github.com/uwplse/verdi https://github.com/uwplse/verdi), which has proved Raft correct in Coq. I imagine handling Byzantine faults and the full complexity of SCP would be quite a bit harder, but probably doable. To me, though, it would be more interesting to prove the implementation correct. Rather than trying to prove an existing C++ implementation correct, it's probably more feasible to reimplement the algorithm within Coq and extract to runnable code. Verdi already supports that, but unfortunately it doesn't support disk state.