By Fabrizio Montesi. Created on: 19 May 2023. See also: Introduction to Choreographies and Choreographic Programming (Wikipedia)
Choreographic Programming is a programming paradigm where programs are choreographies [Montesi 2013]. A choreographic programming language is a special case of a choreographic language. A program given in a choreographic programming language is called choreographic program, or simply choreography when it is clear from the context.
Alice.modPow(g, a, p) -> Bob.x;
Bob.modPow(g, b, p) -> Alice.y;
A snippet of the Diffie-Hellman protocol for key exchange, given in the language of Recursive Choreographies.
Choreographic programming languages are typically accompanied by a compiler, which translates choreographies into executable code for concurrent and distributed systems [Montesi 2023]. The theory of endpoint projection (EPP for short) usually plays an important role in such compilers, in addition to the details of the target executable language. The name 'endpoint projection' was originally introduced by Carbone et al. [2012].
Code for Alice:
send modPow(g, a, p) to Bob;
recv y from Bob;
Code for Bob:
recv x from Alice;
send modPow(g, b, p) to Alice;
Implementations of Alice and Bob compiled from the previous choreography, given in pseudocode.
Carbone, M., Honda, K., Yoshida, N. [2012], 'Structured Communication-Centered Programming for Web Services', ACM Trans. Program. Lang. Syst. 34(2): 8:1-8:78. https://doi.org/10.1145/2220365.2220367
Montesi, F. [2013], 'Choreographic Programming', PhD Thesis, IT University of Copenhagen. https://www.fabriziomontesi.com/files/choreographic-programming.pdf
Montesi, F. [2023], 'Introduction to Choreographies', Cambridge University Press. https://doi.org/10.1017/9781108981491