4 ms·

This reminds me of Oracle’s SCN which blew my mind back in ~2009 when I moved up from mysql home gamer stuff to the corporate world. > Even long edit histories

This reminds me of Oracle’s SCN which blew my mind back in ~2009 when I moved up from mysql home gamer stuff to the corporate world. > Even long edit histories barely compare to the memory savings Zed obtains from not being built with Electron. I got a good chuckle out of this. Speaking of performance, I think it’s I nteresting that ms word and google docs are still using OT rather than CRDT. The goog version seems to work well but I have had nothing but frustration with ms word. Bad merges and weird states are typical, particularly from the fat client. Anyone else interested in the background of OT vs CRDT might find this thread useful: https://news.ycombinator.com/item?id=18191867 https://news.ycombinator.com/item?id=18191867

josephg 4y ago
> The goog version seems to work well but I have had nothing but frustration with ms word. Bad merges and weird states are typical, particularly from the fat client. Argh not getting this stuff right is really frustrating. I've been working on collaborative editing for over a decade now, and I still can't implement any of these algorithms correctly without the help of a fuzz testing. But fuzz testing done right finds all of these problems! There's no excuse! Fuzzers work so well here because all of these algorithms have a clear correctness criteria: After syncing, state should always converge to the same result. So its pretty easy to write code which does this in a loop: 1. Generates some random changes on some fake "peers" 2. Picks 2 peers at random and sync their changes, using your new fancy synchronization algorithm 3. Assert that the state has converged between the peers I've been working on this stuff for over a decade. I've implemented dozens of these algorithms. And every single time I write a fuzzy boi to check my work I find convergence bugs. Playing whack-a-mole with a fuzzer is a rite of passage for implementing systems like this. When your fuzzer runs all night, you should never have lingering convergence bugs like you're describing with Word. As an example, here's a simple fuzzer for a reference list CRDT implementation: https://github.com/josephg/reference-crdts/blob/9f4f9c3a97b497e2df8ae4473d1e521d3c3bf2d2/test.ts#L262-L318 https://github.com/josephg/reference-crdts/blob/9f4f9c3a97b4... The code is so small it almost fits on my laptop screen.
- auggierose 4y ago
  Maybe it is time to do some theorem proving for code like this. Also shows the obvious waste in modern software development: A decade is plenty of time to formally verify a dozen such algorithms. We need to make it easier to do it in a production environment.
  - josephg 4y ago
    Maybe. I honestly don’t know enough about theorum proving. One nice thing about fuzz testing is that it tests both the concepts and the specific implementation. Probably 70% of bugs my fuzzers have found over the years are edge cases my code is handling incorrectly. If I made a “pure” model of my sync engine, wouldn’t I also, still, need to prove my actual implementation matches that model?
    - auggierose 4y ago
      Ideally (part of) your model would already be executable, so that there is no separate implementation. Why have a separate implementation in C, JS, Java, Go, Dart, Swift, Rust, ..., if you have already something much cleaner which you have proven to be correct?

josephg 4y ago

> The goog version seems to work well but I have had nothing but frustration with ms word. Bad merges and weird states are typical, particularly from the fat client. Argh not getting this stuff right is really frustrating. I've been working on collaborative editing for over a decade now, and I still can't implement any of these algorithms correctly without the help of a fuzz testing. But fuzz testing done right finds all of these problems! There's no excuse! Fuzzers work so well here because all of these algorithms have a clear correctness criteria: After syncing, state should always converge to the same result. So its pretty easy to write code which does this in a loop: 1. Generates some random changes on some fake "peers" 2. Picks 2 peers at random and sync their changes, using your new fancy synchronization algorithm 3. Assert that the state has converged between the peers I've been working on this stuff for over a decade. I've implemented dozens of these algorithms. And every single time I write a fuzzy boi to check my work I find convergence bugs. Playing whack-a-mole with a fuzzer is a rite of passage for implementing systems like this. When your fuzzer runs all night, you should never have lingering convergence bugs like you're describing with Word. As an example, here's a simple fuzzer for a reference list CRDT implementation: https://github.com/josephg/reference-crdts/blob/9f4f9c3a97b497e2df8ae4473d1e521d3c3bf2d2/test.ts#L262-L318 https://github.com/josephg/reference-crdts/blob/9f4f9c3a97b4... The code is so small it almost fits on my laptop screen.

auggierose 4y ago
Maybe it is time to do some theorem proving for code like this. Also shows the obvious waste in modern software development: A decade is plenty of time to formally verify a dozen such algorithms. We need to make it easier to do it in a production environment.
- josephg 4y ago
  Maybe. I honestly don’t know enough about theorum proving. One nice thing about fuzz testing is that it tests both the concepts and the specific implementation. Probably 70% of bugs my fuzzers have found over the years are edge cases my code is handling incorrectly. If I made a “pure” model of my sync engine, wouldn’t I also, still, need to prove my actual implementation matches that model?
  - auggierose 4y ago
    Ideally (part of) your model would already be executable, so that there is no separate implementation. Why have a separate implementation in C, JS, Java, Go, Dart, Swift, Rust, ..., if you have already something much cleaner which you have proven to be correct?