| No points were missed - the paper just showed why the points are wrong. I'd be happy to discuss them if you care to read it: there are three concrete correctness problems with CRDT (Logoot) in sections 4.2.4 - 4.2.6. Re: the articles you cited: Molli et al.'s http://hal.inria.fr/inria-00071213/ (A) and their earlier paper: https://www.lri.fr/~mbl/ENS/CSCW/2013/papers/Imine-ECSCW03.p... (B), are unfortunately wrong about OT correctness, demonstrably so. The formalism can obscure the underlying argument, but both A and B uses the same reasoning, which goes something like this: 1. Assumption: An OT system's transformation functions must always satisfy TP1 and TP2, independent of the OT algorithm or protocol, otherwise they are incorrect. 2. Proof: take any existing OT system, disregard the OT algorithm or protocol, just look at the OT transformation functions in isolation, and show that the functions do not satisfy TP1 and TP2. 3. Conclusion: All known OT systems are incorrect The starting assumption of the proof is a false premise: OT's transformation functions do not always require TP2. The proof itself, of evaluating correctness on a subset of OT in isolation, then broadly generalize to OT as a whole, is a sleight of hand (and sloppy theory work). Hence, the conclusion is plainly wrong. TP2 is only required under a very specific pre-condition, and meaning that avoiding this pre-condition means removing the need to preserve TP2 at the level of transformation functions. TP2/CP2-avoidance strategy is commonly used in many OT algorithms and protocols: GOT, JUPITER, G-WAVE/DOCS, COT, TIBOT etc., which are provably correct (see https://www.computer.org/csdl/trans/td/2016/03/07060680-abs..... Transformation functions capable of preserving TP2/CP2 for string-wise text editing (with verified correctness and without tombstones or other meta-data)are also available (see https://dl.acm.org/citation.cfm?doid=2998181.2998252) What I also find really dubious is the verification method used in A and B: paper B starts with using a theorem prover to definitively prove that all previously known OT systems are wrong. Then the paper proposed new transformation functions that the same theorem prover showed to be definitively correct. Paper A, which came after paper B by the same authors, used another theorem prover to show again that all previously known OT functions to be wrong, definitively, including the ones that they proposed to be "definitely correct" from B. So A basically contradicts the results in B, and both were definitively "proven correct". |