Comment by auggierose
1 day ago
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.
1 day ago
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.
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/
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/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
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.
Could you elaborate on that or share a source? It sounds like it'd be not just interesting but important to learn.
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.