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 \emph{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 $\lambda^{\pi}_{\leq}$, with
a new blend of \emph{behavioural types} (from $\pi$-calculus
theory), and \emph{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 \emph{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.