Choreographic Programming

Problem. Choreographic languages and multitier languages both describe a multiparty system as one program instead of many separate ones, but they grew out of different theories (process calculi vs. lambda calculus) in two communities that had little contact, so it was unclear whether results from one side could transfer to the other.

Idea. Two things separate them. The first is perspective: a choreography describes the system objectively, from the outside, like a play script naming every role; a multitier program describes it subjectively, hopping from one participant’s first-person viewpoint to another’s. The second is how communication is modelled: manifest in a choreography, where every interaction is written down, and non-manifest in a multitier program, where it is implied by where values are used.

Fig. 1/2 from the paper.

Result. Once both differences are isolated, translation algorithms in each direction follow, given for Mini Choral and Mini ScalaLoci, minimal languages stripped to the essentials of each paradigm. That opens the door to sharing results across the two communities: compiling a choreography via a multitier compiler to reuse its per-participant code generation, say, or translating a multitier program into a choreography to check statically that it only performs its intended communications.

Links: ECOOP 2021 · paper · video 🏅 Distinguished Paper

Problem. A decentralized app splits contract and client into two separate programs (e.g. Solidity and JavaScript), so their interaction protocol only exists as a convention in the programmers’ heads. A client that sends messages out of the intended order can force the contract off-protocol (a common source of exploited, costly bugs).

Idea. Write contract and client as one program, marking each declaration with where it lives, and use a single construct that expresses “the contract actively waits for a specific client to act” as ordinary control flow, instead of a hand-checked convention split across two files.

Result. A compiler splits the single program into a client and a smart contract, with a formal proof that a malicious, attacker-controlled client can never force the compiled contract off the source-level control flow: the protocol is enforced by construction, not by a hand-written state machine.

Links: TOPLAS 2023 · ECOOP 2022 · extended abstract · artifact · github · arxiv

Problem. Formally verifying choreographies in a proof assistant is notoriously painful, because most choreographic languages are functional (receiving a message introduces a fresh variable), and machine-checked proofs about variable binding and substitution end up dominating the whole effort.

Idea. Give every participant a local state of an arbitrary type, and model “receive a message” not as binding a new variable, but as a plain function from (old state, message) to new state (a state transformer). Receiving a message then introduces no binder at all.

Result. A full mechanization (in Lean) proving soundness and completeness of endpoint projection, deadlock freedom, confluence, and a Hoare logic for choreographies, sidestepping the binding and substitution reasoning that usually dominates such a development.

Links: arxiv

Problem. Choreographic libraries embedded in a host language (Haskell, Rust, …) still have a gap: a “located” value that a role may or may not own is modelled as an option type, and unwrapping it always keeps a dead “impossible” branch (ruled out only by the library author’s discipline, never by the type checker).

Idea. In a dependently-typed host language, make “this role owns this value” a genuine machine-checked proof rather than a runtime tag: a located value’s type carries a proof that the current role is among its owners.

Result. A choreographic library where no error/undefined appears anywhere in the core implementation: totality is enforced by the compiler itself, without sacrificing expressivity relative to prior, partial libraries.

Links: arxiv