Programming Support for Local-First Software
summary
Describes Law, a dedicated local-first reactive language that models user and outside-world interactions, encodes invariants (e.g. “≤30 vacation days”), and maps reactors to CRDT-backed sources. Implementation translates affected interactions to the Viper verification back end, finds pairs of conflicting interactions, and synthesizes coordination (or exposes alternatives); compiles to Scala and verifies small case studies in ~5s and TPCC scenarios in ~15s. Trade-offs include added synchronization and the need to author invariants.
AI-written summary · about
chapters (6)
- 0:00Start
- 3:16The Case for Local-First Software
- 4:29Quick CRDT Intro
- 8:32Programming Abstractions
- 11:46Architecture and Implementation
- 16:11Future Work
related talks
24mGoing Local-First: A Primer
26mLocal-first
41mTowards language support for distributed systems
01h 30mImplementing, verifying and debugging distributed event-based systems
32mCan local-first really scale at the edge?
41mDeclarative, Convergent Edge Computation
21mCRDTs for Mortals
18mRethinking Apps with Local-First Architecture