Choreographic programming in Elixir

That’s very neat—it’s in an entirely different realm however. Good luck building it!

I’ve recently started working on something that I think is applicable. See GitHub - CharlesIrvineKC/mozart · GitHub.

The first linked paper: “Real-Word Choreographic Programming”

Hi @ashton314 - very interesting thread. Please may I ask where you first came across the term choreographic programming?

Pirouette seems interesting, but the assumptions it makes seem to diverge somewhat from practical reality

You might have noticed that Pirouette is mostly concerned with making sure that the guarantees of choreographic programming hold in an ideal scenario—if they didn’t we’d be in trouble. Instantaneous and certain messages seems reasonable when you’re running on a single machine—unless there’s some other underlying bug in the BEAM.

Extending the formalism to account for self-sent messages wouldn’t be all that difficult. This idiom is certainly convenient with BEAM languages; I would argue that it’s not essential to concurrent programming so it’s understandable why the authors chose this. Again, that doesn’t mean we couldn’t adapt the findings from this paper to BEAM languages.

Real-World Choreographic Programming
the one thing that isn’t in the paper is the actual choreography

It is, actually—though it’s a little tricky to spot. On the first page there are two badges about the artifact. (In this case, that’s the source for the IRC server/client & choreography.) You can click on those to get a link to where the artifact is hosted on Zenodo: Accepted Artifact for Real-World Choreographic Programming: Full-Duplex Asynchrony and Interoperability | Zenodo. This is typical for most research papers; most journals and conferences would prefer a full code listing separate rather than embedded in a PDF. I agree it would have been nice to see more snippets from the choreography in this paper, but I can understand also why the authors did it the way they did.

Pirouette seems interesting, but the assumptions it makes seem to diverge somewhat from practical reality:

• in 2.2: “Message sending is instantaneous and certain: messages do not get lost in the air.”
• in 3.1, referencing the conditions on the SendE rule: “The second check reflects the fact that sends from a node to itself is not meaningful.”

That latter one would come as a surprise to most BEAM developers

Agreed that it’s an interesting read, but the one thing that isn’t in that paper is the actual choreography! It’s tricky to evaluate a technique’s expressiveness without seeing it express things.

Choreographies differ significantly and materially from the UML-based code generation you’re describing. I agree that kind of tool makes things harder to maintain. Choreographies are code, though, so they don’t have the same drawbacks. If you (or anyone else) would like to see more about choreographies, these papers are useful:

• https://doi.org/10.1145/3498684
• Real-World Choreographic Programming: Full-Duplex Asynchrony and Interoperability (I already posted this one; this is a neat one because they describe in detail how to solve a real problem with choreographic programming.)

The one thing I would love to see however, is a visual representation of this from the written code. A lot of times it becomes hard to reason about a collection of processes interacting between each-other, ideally in a format like cisco packet tracer, where you can also see everything happening in real-time.

Have you tried Observer?

One of the other compelling things about choreographies is having an overview of how all the parties in a system talk to each other.

TLA+ and choreographic programming are related in the sense that they both work with concurrent systems, but CP gets you a correct-by-construction implementation. TLA+ is “just” for model checking. (Still super useful and really cool! Glad to see TLA+ is known to some other folks.)

So far that’s kind of sci-fi I am afraid, at least from the point of view of the classic / mainstream programming.

I should have been more clear (and maybe this will clear up some of the confusion I’ve been seeing from others): I am a programming languages researcher. I am not looking for some tool to solve some concrete problem. My job is to make this “sci-fi” a reality.

Choreographic programming is a new paradigm that can solve whole classes of bugs, and I’m experimenting with CP and Elixir. Everyone is going to have some tacit choreography in their programs; CP as a paradigm brings these protocols/agreements/choreographies to the forefront and treats them as a thing in and of themselves.

I need to know if someone has encountered a library to do the automatic choreography → endpoint projection before. I’m pretty sure the answer is “no” since no one has mentioned a concrete library.

All the tools y’all have mentioned suggest that solving concurrency bugs is something you have on your minds. That’s good because it means there’s a need that this might fill!

Yep, it’s not a real programming language yet. But I appreciate the declarative approach. IMO it’s the future. But we don’t seem to be there yet.

Fwiw, TLA+ is a language (and toolchain) for describing algorithms and not code. It shines for concurrent algorithms, but is equally useful for the state machine approach to computation in general (it views the latter as a generalisation of the former in any case)