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.
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 having the same left origin. That rule is hard to describe but can eventually be proved commutative; I'm hoping to include this in a paper someday.
[1] https://josephg.com/blog/crdts-are-the-future/
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.