Concurrent and distributed programming is notoriously hard.
Modern languages and toolkits ease this difficulty by offering
message-passing abstractions, such as actors (e.g., Erlang,
Akka, Orleans) or processes (e.g., Go): they allow for simpler
reasoning w.r.t. shared-memory concurrency, but do not
ensure that a program implements a given specification.
To address this challenge, it would be desirable to specify
and verify the intended behaviour of message-passing applications
using types, and ensure that, if a program type-checks
and compiles, then it will run and communicate as desired.
We develop this idea in theory and practice. We formalise
a concurrent functional language λπ
⩽, with a new blend of
behavioural types (from π-calculus theory), and dependent
function types (from the Dotty programming language, a.k.a.
the future Scala 3). Our theory yields four main payoffs: (1) it
verifies safety and liveness properties of programs via type–
level model checking; (2) unlike previous work, it accurately
verifies channel-passing (covering a typical pattern of actor
programs) and higher-order interaction (i.e., sending/receiving
mobile code); (3) it is directly embedded in Dotty, as a
toolkit called Effpi, offering a simplified actor-based API;
(4) it enables an efficient runtime system for Effpi, for highly
concurrent programs with millions of processes/actors.