3 ms·
> Lamport did comment on it (via email) saying that understanding Paxos is less important than proving it works (via TLA+). I suppose that's not wrong; if I kn
by tombert 5y ago
> Lamport did comment on it (via email) saying that understanding Paxos is less important than proving it works (via TLA+).
I suppose that's not wrong; if I know for a fact that something is going to behave how I expect it too, I don't generally care how it works. I can treat the algorithm as a black box and just go from there.
That said, I dont' completely agree. If I am implementing Paxos in NewLangOfTheMonth, it's likely that a straight one-to-one port of another version will not fully work due to tiny differences in the language semantics. If I don't understand Paxos, then it's unlikely I'll be able to correct any mistakes in the implementation.
- skrtskrt 5y agoAgreed, being able to trust it is probably what I want in order to use it at my job to get shit done - being able to understand it/implement it is what I want to do on my own time. Unless you're one of the rare group who gets paid to implement it in x language/library/technology, it's more of a mental exercise than anything, something nice to go "ahhh cool!" when you understand it, then move on.
- uvdn7 5y agoYeah I agree. I think understanding the protocol makes it much less likely to introduce protocol level bugs during implementation. E.g. why certain steps need to be done in certain order.