This lightning talk presents and demonstrates a new prototype communication-checking tool for Erlang codebases: Mailboxer. Distributed software is hugely important to modern economies, yet it is vulnerable to communication errors. Behavioural types can detect such errors statically (at compile time), but there has been a mismatch between these type systems and the actor paradigm. Mailbox types are a novel behavioural type system designed specifically for actors, addressing this gap. We have developed the first language design incorporating mailbox type-checking via a sophisticated algorithm [1], and are building Mailboxer, a freestanding checker for Erlang. By annotating parts of a codebase with expected message types, Mailboxer can detect unreceived messages, some deadlocks, protocol violations, or message tag typos, thus reducing development/debugging time.
While we currently target Erlang, the type theory and checking technology apply to other mailbox-based actor languages, including Elixir and Scala/Akka. In summary, mailbox annotations embed and document process communication, and the prototype already scales to multiple protocols and common paradigms.

This is joint work with Duncan Paul Attard, Simon Fowler, Simon J. Gay, and Phil Trinder, and is part of the STARDUST project https://epsrc-stardust.github.io/

[1] Fowler S., Attard D., Sowul F., Gay S., Trinder P. Special Delivery: Programming with Mailbox Types. Proc. ACM on Programming Languages 7(ICFP), September 2023