Choreographic Programming: its essence, beauty, and necessity
summary
Claims a communication-first programming model where a choreography compiles to correct per-participant code, yielding deadlock freedom by construction. Implements a compiler chain and prototypes: an embedded DSL (hcore) and a practical Coral Java extension that annotates types with locations and generates runnable libraries. Provides an amendment transformation that injects extra messages to make unrealizable choreographies projectable. Presents empirical artifacts, ongoing ERC-funded work on logics, smarter compilers and a benchmark suite.
AI-written summary · about
chapters (21)
- 0:00Choreographic programming intro
- 3:35Concurrent code unpredictability
- 6:22Core idea of choreography
- 10:16Compiler properties key
- 13:25History of notation
- 16:42Evolution milestones
- 18:52Formalizing paradigm
- 23:41Coral language first
- 25:49Choreographies in functional programming
- 27:12Embedded choreographic langs
- 28:35Core language principles
- 29:21Translation questions
- 33:56Beyond technicalities
- 37:12Art inspired by choreos
- 40:42Future directions
- 48:34Q&A: Session types
- 51:02Q&A: HPC patterns
- 54:15Q&A: Actor languages
- 56:28Q&A: Dynamic participants
- 59:42Q&A: Runtime checks
- 1:00:25Q&A: Hardware applications
related talks
01h 24mProcedural Programming: It’s Back? It Never Went Away
33mOrchestrate Your Choreography
01h 02mProcedural Programming: It Never Went Away
42mOrchestration vs Choreography, A Guide To Composing Your Monolith
01h 01mProgramming Abstractions for Orchestration of HPC Scientific Computing
01h 05mVerifying Infinitely Many Programs at Once
40mCode is your partner in thought
52mThink Abstractly, Work Concretely