Local-first software manages and processes private data locally while still enabling collaboration between multiple parties connected via partially unreliable networks. Such software typically involves interactions with users and the execution environment (the outside world). The decentralized nature of local-first software paired with the unpredictability of interactions driven from the outside world impede reasoning about their correctness. Yet, existing solutions to develop local-first software do not provide safety guarantees and instead expect developers to reason about concurrent interactions in an environment with unreliable network conditions. This is too much to ask of application developers, who are usually not experts in designing distributed systems.

This work seeks to develop a programming model which facilitates the construction of local-first software and eradicates certain classes of safety and security problems by design. We do so by providing a dedicated local-first programming language and an accompanying automated verification procedure that can be integrated as part of the compilation process.