One thing I don’t understand is how you can guarantee the lack of a distributed deadlock. I’m sure it’s covered in the underlying research, but just conceptually it’s hard to picture.

What stops a choreography where Claire send a message to Bob but Bob is waiting for Alice and Alice is waiting for Claire?

Is it like Rust memory safety where not all valid programs are accepted but all invalid programs are rejected?

I think some examples of the distributed code in action on a trivial and non trivial distributed example is more compelling than a 3d donut render

You can think about it as a protocol.

The protocol doesn't describe "Claire sends" and "Bob receives" as two independent actions that wait for each other, it describes them as a single communication in the global program/state.

When it gets executed into code, every send already has a corresponding receive by construction, so you can't write something like "Claire sends to Bob while Bob is actually waiting for Alice" unless the protocol itself allowed that execution.

So the cycle you're describing can't just accidentally appear because of sync issues, because the assumption is a communication is represented correctly at each turn.

So yeah it kinda does limit the set of all possible programs since I would expect not everything can be encoded this way also seems hard to resolve this in practice without only allowing communication b/w Wyzer systems.

I am not very familiar with this topic in practice so OP would be the best person to answer this, I am quite intrigued by how it works in practice as well.

hmm, I suspect distributed systems can be modelled with a form of probabilistic borrow-checking as long as you have control all the connected systems.

This question is in fact core to research in the paradigm. Let me first address how it works and then the expressivity question.

A choreographic programming language features programming abstractions for programming communication intent. For example, often they have a primitive like:

Alice.expr -> Bob.x

read 'Alice communicates the evaluation of expr to Bob, which stores the message in its local variable x'. (In fact, we discovered that we can extend any mainstream language to have this kind of high-level primitives by extending data types with locations, see choral-lang.org).

This makes it impossible to write mismatched communication actions, because you're expressing both the send and receive actions in a single atomic instruction: they are well-matched by construction. You then build a compiler (typically called 'projection') that generates distributed programs for Alice and Bob -- the former doing the send to Bob and the latter doing the receive from Alice. We like making formal models of these compilers and mathematically proving them correct. A compiler that respects the choreography then automatically entails deadlock-freedom of the compiled code without the need for complex checks, because the source choreography cannot syntactically express deadlocked terms.

Consequently, there are no deadlocked distributed programs that we can compile from choreographies. It's an application of the neat trick of designing high-level languages for 'guiding' programming: instead of programming a distributed system with low-level primitives and then attempting the generally very hard task of checking for deadlocks, we use a high-level language where deadlocks cannot be written (or are at least easy to check against).

The above hopefully explains the intuition of how choreographic programming works. But then, as you did, one naturally asks: What can we express in choreographic programming languages? Are there fundamental limitations?

We do not know exactly yet; this is an area of very active exploration. Over the years, people have developed more and more clever choreographic programming languages that capture more and more interaction patterns.

What's perhaps surprising is that, for some theories of distributed languages (or interaction patterns, if you like), we know that choreographic programming is complete, in the sense that it can capture all deadlock-free systems that can be modelled in those theories. The first result of this kind was about capturing all interaction behaviours that can be described in linear logic (in the Curry-Howard interpretation of it with process calculi), but there are also works that can deal with recursive behaviour and even process spawning (fork). That's encouraging.

I think that investigating what the paradigm precisely can and cannot do is fascinating (but I'm very biased here..), not least because using a mathematically-modelled compiler lets us optimise the generated code aggressively (e.g., adding more asynchrony, as in Ozone). From the state of the art already out there, it looks like choreographic programming is 'expressive enough' for many different purposes. Hopefully it's gonna be the typical situation with high-level abstractions, whereby for most cases and most people the high-level language is gonna be good and low-level communication actions will be necessary only in niche scenarios. In the meantime, there are choreographic languages that can be integrated with middleware and foreign APIs to cover up for deficiencies (like Choral, HasChor, etc.).