Toward Verified Library-Level Choreographic Programming with Algebraic Effects

TL;DR

This paper introduces a formal foundation for library-level choreographic programming using algebraic effects, enabling reasoning about correctness and implementing a prototype in Agda.

Contribution

It models library-level CP with algebraic effects, providing a theoretical basis and correctness proofs for EPP in this context.

Findings

Prototype implementation in Agda demonstrates feasibility.

Algebraic effects facilitate reasoning about correctness.

Framework supports verifying soundness and completeness.

Abstract

Choreographic programming (CP) is a paradigm for programming distributed applications as single, unified programs, called choreographies, that are then compiled to node-local programs via endpoint projection (EPP). Recently, library-level CP frameworks have emerged, in which choreographies and EPP are expressed as constructs in an existing host language. So far, however, library-level CP lacks a solid theoretical foundation. In this paper, we propose modeling library-level CP using algebraic effects, an abstraction that generalizes the approach taken by existing CP libraries. Algebraic effects let us define choreographies as computations with user-defined effects and EPP as location-specific effect handlers. Algebraic effects also lend themselves to reasoning about correctness properties, such as soundness and completeness of EPP. We present a prototype of a library-level CP framework based on algebraic effects, implemented in the Agda proof assistant, and discuss our ongoing work on leveraging the algebraic-effects-based approach to prove the correctness of our library-level CP implementation.