The gist is, you give the synthesizer a C++ implementation of a regular plain-old data structure along with a few annotations, and the synthesizer will synthesize a CRDT implementation of that data structure automatically that is provably-correct. The input needs to be in C++ using only a few types like int, set, etc, because the synthesizer's analysis is implemented against LLVM IR.
The driving example is taking a trivial implementation of a set, and getting back different CRDT implementation of sets depending on the annotations that guide the synthesis.
So, who is this for? A productionized version could be used by feature programmers who want to build new collaborative features. They can "just" write the feature for a single machine, and have the synthesis make it collaborative.
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.
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?