Programming and Proving with Distributed Protocols

Watch a conference presentation from POPL 2018 exploring Disel, a groundbreaking framework for implementing and verifying distributed systems within the Coq proof assistant. Learn how this innovative approach allows developers to create distributed systems using a domain-specific language while ensuring protocol compliance through dependent type systems. Discover how Disel's Hoare-style program logic enables interactive verification of system implementations and supports modular composition of verified components. Follow along as the speakers demonstrate practical examples of using Disel to build reliable distributed systems, discuss its underlying logic and metatheory, and share their experiences with this powerful verification framework. Gain insights into addressing key challenges in distributed systems development, including correct implementation of core components and trustworthy composition of standalone elements into larger applications.