Abstract
Over the past two decades, there has been a variety of work connecting distributed computing concerns (e.g., consistency, fault tolerance, parallelization) to formal representations of programs. This includes work grounded in logic, including the CALM Theorem and related results. It also includes work grounded in algebra, notably the semi-lattices embraced in CRDTs. Many of these results have also been embedded in Datalog extensions, which are increasingly viewed through the lens of semirings. Ideally we should unify these results and be able to move fluidly between the formalisms as needed, both formally (for proving things) and in practical language stacks (for programming, program checking, and compilation.) As a practitioner, I will motivate and survey some of what's been done to date in the systems world, and raise some open questions, based on our experience with language/runtime designs including Dedalus, Bloom and our current Hydro project.