This sounds interesting but makes my eyes glaze, even as someone actively working with CRDTs as an end-user developer. And that's okay! But can someone translate this to mortal?<p>My weak attempt to parse this leaves me with the impression that the goals are conceptually similar to the Elm language compiler, where if you can stay in your lane (so to speak), you are given assurances about immutability and the theoretical impossibility of run-time errors.<p>If I'm way off, well... now you know why I'm asking for an assist. Who is this for, and what do they do with it? Is it a cool proof or something with practical implications?
From the abstract: "In this paper, we present Katara, a program synthesis-based system that takes sequential data type implementations and automatically synthesizes verified CRDT designs from them. Key to this process is a new formal definition of CRDT correctness that combines a reference sequential type with a lightweight ordering constraint that resolves conflicts between non-commutative operations."
The synthesis is amazing! But, I would like to see an attempt to synthesize a rich text CRDT rather than the relatively trivial set & LRW register stuff.