3 ms·

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 translat

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?

jitl 4y ago
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.
- alexvoda 4y ago
  Since it takes LLVM IR as input, why can it not take a subset of Rust or other LLVM supported language?
  - shadaj 4y ago
    Katara author here, you're right! Katara is built on Metalift (https://github.com/metalift/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!

jitl 4y ago

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.

alexvoda 4y ago
Since it takes LLVM IR as input, why can it not take a subset of Rust or other LLVM supported language?
- shadaj 4y ago
  Katara author here, you're right! Katara is built on Metalift (https://github.com/metalift/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!