4 ms·

And let's not forget that the official paper on Yjs is just plain wrong, the "proofs" it contains are circular. They look nice, but they are wrong.

breakingcups 7mo ago
Could you elaborate on that or share a source? It sounds like it'd be not just interesting but important to learn.
- auggierose 7mo ago
  https://dl.acm.org/doi/epdf/10.1145/2957276.2957310 https://dl.acm.org/doi/epdf/10.1145/2957276.2957310 Try to understand 3.1-3.4 in this paper, and you'll find that the correctness proof doesn't prove anything. In particular, when they define <_c, they do this in terms of rule1, rule2, and rule3, but these are defined in terms of <_c, so this is just a circular definition, and therefore actually not a definition at all, but just wishful thinking. They then prove that <_c is a total order, but that proof doesn't matter, because <_c does not exist with the given properties in the first place.
mweidner 7mo ago
This was my impression as well. If you ignore the paper and just look at the source code - and carefully study Seph Gentle's Yjs-like RGA implementation [1] - I believe you find that it is equivalent to an RGA-style tree, but with a different rule for sorting insertions that have the same left origin. That rule is hard to describe, but with some effort one can prove that concurrent insertions commute; I'm hoping to include this in a paper someday. [1] https://josephg.com/blog/crdts-are-the-future/ https://josephg.com/blog/crdts-are-the-future/
- josephg 7mo ago
  Yes, I think it would be a good paper. I made a tiny self contained implementation of this algorithm here if anyone is curious: https://github.com/josephg/crdt-from-scratch/blob/master/crdt.ts https://github.com/josephg/crdt-from-scratch/blob/master/crd... FugueMax (or Yjs) fit in a few hundred lines of code. This approach also performs well (better than a tree based structure). And there's a laundry list of ways this code can be optimised if you want better performance. If anyone is interested in how this code works, I programmed it live on camera in a couple hours: https://www.youtube.com/watch?v=_lQ2Q4Kzi1I https://www.youtube.com/watch?v=_lQ2Q4Kzi1I This implementation approach comes from Yjs. The YATA (yjs) academic paper has several problems. But Yjs's actual implementation is very clever and I'm quite confident its correct.

breakingcups 7mo ago

Could you elaborate on that or share a source? It sounds like it'd be not just interesting but important to learn.

auggierose 7mo ago
https://dl.acm.org/doi/epdf/10.1145/2957276.2957310 https://dl.acm.org/doi/epdf/10.1145/2957276.2957310 Try to understand 3.1-3.4 in this paper, and you'll find that the correctness proof doesn't prove anything. In particular, when they define <_c, they do this in terms of rule1, rule2, and rule3, but these are defined in terms of <_c, so this is just a circular definition, and therefore actually not a definition at all, but just wishful thinking. They then prove that <_c is a total order, but that proof doesn't matter, because <_c does not exist with the given properties in the first place.

mweidner 7mo ago

This was my impression as well. If you ignore the paper and just look at the source code - and carefully study Seph Gentle's Yjs-like RGA implementation [1] - I believe you find that it is equivalent to an RGA-style tree, but with a different rule for sorting insertions that have the same left origin. That rule is hard to describe, but with some effort one can prove that concurrent insertions commute; I'm hoping to include this in a paper someday. [1] https://josephg.com/blog/crdts-are-the-future/ https://josephg.com/blog/crdts-are-the-future/

josephg 7mo ago
Yes, I think it would be a good paper. I made a tiny self contained implementation of this algorithm here if anyone is curious: https://github.com/josephg/crdt-from-scratch/blob/master/crdt.ts https://github.com/josephg/crdt-from-scratch/blob/master/crd... FugueMax (or Yjs) fit in a few hundred lines of code. This approach also performs well (better than a tree based structure). And there's a laundry list of ways this code can be optimised if you want better performance. If anyone is interested in how this code works, I programmed it live on camera in a couple hours: https://www.youtube.com/watch?v=_lQ2Q4Kzi1I https://www.youtube.com/watch?v=_lQ2Q4Kzi1I This implementation approach comes from Yjs. The YATA (yjs) academic paper has several problems. But Yjs's actual implementation is very clever and I'm quite confident its correct.