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.
Really nice article. I think the undo/redo for rich text is a tad bit more complicated than undo/redo for objects with properties.
For starters, in your demo when user A has selected some word and user B writes a letter in it, user A lost the selection. And this isn't even undo/redo yet, just normal collaborative thing.
That "some extra plumbing" you mention is quite big. Please don't get me wrong here – I would love to see you pull it off – Liveblocks.io seems like a good platform from what I read & heard, but you underestimate how hard that problem might be.
Notion’s selection and undo/redo with multiplayer are pretty potato. Notion stores selection as grapheme indexes in a text property, so while it won’t lose selection if someone adds/removed characters from a text, your selection won’t make as much sense as one in Google Docs. Likewise with undo/redo or regular typing into the same field - it’s all last-write-wins updates.
On the other hand, Notion’s editor does a much better job with CJK input, Android, etc compared to Slate. Slate has a beautiful API design but its implementation suffers outside of ideal conditions.
Awesome to hear from the Notion team who really gets this deeply.
Slate definitely has its own limitations, especially when used on non desktop devices. Seems like ProseMirror would be a good open source alternative to Slate, what do you think?
ProseMirror did the best the last time I tested these libraries. TipTap (a competitor of yours?) provides an API layer on top, which I haven’t spent much time investigating. For my purpose I don’t want intermediary abstractions - but might be useful for your context depending on how much you want to specialize in rich text.
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?
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?
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.
Katara author here, you're right! Katara is built on Metalift (https://github.com/metalift/metalift), which is a general purpose framework we've been building at Berkeley to abstract away the logic of analyzing the LLVM IR. The decision to use LLVM was exactly because it is the least-common-denominator for so so many languages, so we are excited to add official support for Rust and friends in the near future!
20 comments
[ 3.2 ms ] story [ 57.8 ms ] thread(and yes, it is very complex lol)
Our open-source block-based text editor could support it too with some extra pluming (which we haven’t got to yet).
We’re planning to add this in as more and more developers are looking to port this experience into their own products.
Is there anything else you’d like this example to support?
Thanks for the feedback! :)
For starters, in your demo when user A has selected some word and user B writes a letter in it, user A lost the selection. And this isn't even undo/redo yet, just normal collaborative thing.
That "some extra plumbing" you mention is quite big. Please don't get me wrong here – I would love to see you pull it off – Liveblocks.io seems like a good platform from what I read & heard, but you underestimate how hard that problem might be.
On the other hand, Notion’s editor does a much better job with CJK input, Android, etc compared to Slate. Slate has a beautiful API design but its implementation suffers outside of ideal conditions.
Source: I built this: https://twitter.com/jitl/status/1483918085384028163?s=46&t=S...
Slate definitely has its own limitations, especially when used on non desktop devices. Seems like ProseMirror would be a good open source alternative to Slate, what do you think?
Supporting multiplayer collaboration at the character level is much more difficult and we’re very well aware of that :)
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?
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.