Mixed Choices: Taming Failures with Session Types in Erlang
Erlang, Distributed Systems, Session Types, OTP
Erlang, Distributed Systems, Session Types, OTP
Distributed systems fail. Processes time out. Messages arrive out of order. And yet, these cases are often handled ad hoc in runtime code rather than made explicit in the protocol itself. In this workshop, you'll learn how multiparty session types and mixed choice can model timeouts, exceptions, and race conditions, and how those specifications can be transformed into runnable Erlang OTP state machines.
Distributed systems are notoriously difficult to reason about. Timeouts, failures, and race conditions are often treated as edge cases hidden deep inside application logic. This workshop introduces multiparty session types, a formal approach to describing communication protocols between distributed processes, and shows how mixed choice extends these protocols to model real-world failure scenarios.
Participants will work with a toolchain that validates protocol specifications and generates Erlang gen_statem code, producing OTP-compliant state machines with safety guarantees built in. Through practical examples, attendees will learn how to make protocol structure explicit and avoid implementing delicate concurrency logic by hand.
Basic familiarity with functional programming concepts is expected. Some exposure to concurrent or distributed systems is helpful but not required. No prior knowledge of session types or formal methods is necessary.
Attendees should bring a laptop with Docker installed and running.
gen_statem code.Functional programmers interested in distributed systems, concurrency, protocol design, or formal methods. It is particularly relevant for Erlang and Elixir practitioners, although the ideas apply across languages and platforms.