5 ms·

I think the blog post is valuable, but I'd point out that aphyr is also not publishing formal proofs or utilizing the verification he suggests is necessary. I d

I think the blog post is valuable, but I'd point out that aphyr is also not publishing formal proofs or utilizing the verification he suggests is necessary. I don't think this is intentional, but they should realize and own that they are borrowing authority of formal method they are not demonstrating and then criticizing others for the same lack of demonstration.

aphyr 13y ago
Well this one's proof by construction, so I don't feel the need to go particularly deep into the math. If you prefer a more rigorous approach take a look at the TLA proofs earlier in the Jepsen series; think I linked one on Redis+async replication in the article.
- jasonwatkinspdx 13y ago
  I read and enjoyed them, thanks. I'd just like people to be in a more collaborative vs combative mode, and I think a big part of that is not overly relying on rhetoric or overreaching what you've actually demonstrated. Using formalism on a blog is commendable, but it's also not the same thing as a properly reviewed paper. People should keep straight the levels of dialog here and value them each for the light they shed. This has been mostly a productive exchange despite a few "yer doin' it wrong bro" attitude folks, and I just want to throw my hat in to strongly advocate for keeping it that way.
  - davidw 13y ago
    As a way of checking, when a phrase is in character for "Comic Book Guy", you know it's probably a bit too much on the mean-spirited side of things.
justinsb 13y ago
Isn't the simulation sufficient? A proof that something works requires logic, but a single counter-example suffices to show that something doesn't work.
rdtsc 13y ago
He writes very good partitioning and consistency tests. Those are invaluable. As we have seen most "reliable", "distributed" and "fault tolerant" databases fall to their knees in those tests. I think he is honest and he doesn't fake his result, I believe those are hard corner cases but they are not impossible. Overall it is very good for the industry, better for Aphyr to lose one of his integer key value pairs, make a blog post about it, than for your health insurance to lose your health records.

aphyr 13y ago

Well this one's proof by construction, so I don't feel the need to go particularly deep into the math. If you prefer a more rigorous approach take a look at the TLA proofs earlier in the Jepsen series; think I linked one on Redis+async replication in the article.

jasonwatkinspdx 13y ago
I read and enjoyed them, thanks. I'd just like people to be in a more collaborative vs combative mode, and I think a big part of that is not overly relying on rhetoric or overreaching what you've actually demonstrated. Using formalism on a blog is commendable, but it's also not the same thing as a properly reviewed paper. People should keep straight the levels of dialog here and value them each for the light they shed. This has been mostly a productive exchange despite a few "yer doin' it wrong bro" attitude folks, and I just want to throw my hat in to strongly advocate for keeping it that way.
- davidw 13y ago
  As a way of checking, when a phrase is in character for "Comic Book Guy", you know it's probably a bit too much on the mean-spirited side of things.

justinsb 13y ago

Isn't the simulation sufficient? A proof that something works requires logic, but a single counter-example suffices to show that something doesn't work.

rdtsc 13y ago

He writes very good partitioning and consistency tests. Those are invaluable. As we have seen most "reliable", "distributed" and "fault tolerant" databases fall to their knees in those tests. I think he is honest and he doesn't fake his result, I believe those are hard corner cases but they are not impossible. Overall it is very good for the industry, better for Aphyr to lose one of his integer key value pairs, make a blog post about it, than for your health insurance to lose your health records.