In choreographic programming, developers use achoreographic programming language to define the intended communication behaviour of concurrent participants. Programs in this paradigm are calledchoreographies.[1]Choreographic languages are inspired bysecurity protocol notation (also known as "Alice and Bob" notation). The key to these languages is the communication primitive, for example
Alice.expr -> Bob.x
reads "Alice communicates the result of evaluating the expressionexpr toBob, which stores it in its local variablex".[3]Alice, Bob, etc. are typically calledroles orprocesses.[2]
The choreography starts in Line 1, whereClient communicates a pair consisting of some credentials and the identifier of the service it wishes to access toCAS.CAS stores this pair in its local variableauthRequest (for authentication request).In Line 2, theCAS checks if the request is valid for obtaining an authentication token.If so, it generates a token and communicates aSuccess message containing the token to bothClient andService (Lines 3–5).Otherwise, theCAS informsClient andService that authentication failed, by sending aFailure message (Lines 7–8). We refer to this choreography as the "SSO choreography" in the remainder.
A key feature of choreographic programming is the capability of compiling choreographies to distributed implementations. These implementations can be libraries for software that needs to participate in a computer network by following a protocol,[1][3][4] or standalone distributed programs.[5][6]
The translation of a choreography into distributed programs is calledendpoint projection (EPP for short).[2][3]
Endpoint projection returns a program for each role described in the source choreography.[3] For example, given the choreography above, endpoint projection would return three programs: one forClient, one forService, and one forCAS. They are shown below in pseudocode form, wheresend andrecv are primitives for sending and receiving messages to/from other roles.
Endpoint Projection (EPP) of the SSO choreography
Client
send (credentials, serviceID) to CASrecv result from CAS
Service
recv result from CAS
CAS
recv authRequest from Clientif check(authRequest) then token = genToken(authRequest) send Success(token) to Client send Success(token) to Serviceelse send Failure to Client send Failure to Service
For each role, its code contains the actions that the role should execute to implement the choreography correctly together with the others.
The paradigm of choreographic programming originates from its titular PhD thesis.[7][8][9]The inspiration for the syntax of choreographic programming languages can be traced back tosecurity protocol notation, also known as "Alice and Bob" notation.[1] Choreographic programming has also been heavily influenced by standards forservice choreography andinteraction diagrams, as well as developments of the theory ofprocess calculi.[1][3][10]
Choral (website).[16][17] An object-oriented choreographic programming language that compiles to libraries inJava. Choral is the first choreographic programming language with decentralised data structures and higher-order parameters.
^Cohen, Liron; Kaliszyk, Cezary (2021).Formalising a Turing-Complete Choreographic Language in Coq. Leibniz International Proceedings in Informatics (LIPIcs). Vol. 193. pp. 15:1–15:18.doi:10.4230/LIPIcs.ITP.2021.15.ISBN9783959771887.S2CID231802115.
