Katara: Synthesizing CRDTs with Verified Lifting | Hacker News Reader

Katara: Synthesizing CRDTs with Verified Lifting

arxiv.org

86 pointsRossBencina20 comments

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?

It seems like it could be very practical.

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.

Since it takes LLVM IR as input, why can it not take a subset of Rust or other LLVM supported language?

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!

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."

Github here: https://github.com/hydro-project/katara

For what's worth, Katara means 'curse' in Greek ;)

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.

Doesn't rich text CRDT require messy rules to comply with our collaborative undo-redo mental model?

Some people have already solved that, like Liveblocks.io Here's an example of Notion-like text editor with multiplayer: https://liveblocks.io/examples/block-text-editor-advanced/ne...

(and yes, it is very complex lol)

Nah, Liveblocks.io + Slate is pretty far from Notion-like experience. It doesn't even do local undo/redo.

Liveblocks does support multiplayer undo/redo. We even wrote an interactive blog post about it: https://liveblocks.io/blog/how-to-build-undo-redo-in-a-multi...

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! :)

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.

Source: I built this: https://twitter.com/jitl/status/1483918085384028163?s=46&t=S...

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.

Thank you. I think you misunderstood me. By extra pluming I meant: extra pluming on the block-based text editor as it is.

Supporting multiplayer collaboration at the character level is much more difficult and we’re very well aware of that :)

Hmm… Could you turn the Heap itself into a CRDT?

I think so. Some of us in the braid.org group have been discussing how to add OS syscalls to do so.

Love the Avatar the Last Airbender reference

Reply on news.ycombinator.com