> whereas OT is generally too complicated and unproven to offer that guarantee at all.
Citation needed.
I've built several production-level OT-based systems on top of ShareJS's JSON OT[1] code. The set of operations supported is guaranteed to be conflict-free and correct. We don't have AGDA proofs but we've used fuzzers to ferret out correctness bugs and its been about 2 years since a bug was found in the transform code. All in all, I'm very happy with the implementation.
Meanwhile, I don't believe a more generic JSON OT / CRDT system can be made conflict-free. (Well it can be conflict-free, but you'll lose data if it is). If you support arbitrary tree-level moves, you have the User A moves x into y's children, user B moves y into x's children problem. There are simply no good ways to resolve these operations without user intervention, or a lot more knowledge of the data structures at play.
Citation needed.
I've built several production-level OT-based systems on top of ShareJS's JSON OT[1] code. The set of operations supported is guaranteed to be conflict-free and correct. We don't have AGDA proofs but we've used fuzzers to ferret out correctness bugs and its been about 2 years since a bug was found in the transform code. All in all, I'm very happy with the implementation.
Meanwhile, I don't believe a more generic JSON OT / CRDT system can be made conflict-free. (Well it can be conflict-free, but you'll lose data if it is). If you support arbitrary tree-level moves, you have the User A moves x into y's children, user B moves y into x's children problem. There are simply no good ways to resolve these operations without user intervention, or a lot more knowledge of the data structures at play.
[1] https://github.com/ottypes/json0