The newest zine from my research group, “Carol’s Causal Conundrum”, is out today! You can read it online, or print your own free copies to read offline!

This zine is an introduction to causally ordered message delivery, a fundamental abstraction for distributed programming. It’s the result of a six-month collaboration between my student collaborator, Ayush Manocha, and me. In the zine, we talk about what exactly causally ordered message delivery is, what problem it solves, and a few ways to implement it: two classic ways, and one new way!

I’ve been making research zines collaboratively with undergrads since 2024; “Communicating Chorrectly with a Choreography”, a zine about choreographic programming, was our first one. After the success of that first zine project, I began looking for a student who wanted to work on a follow-up. Ayush, who had just taken my undergrad programming languages course, was keen to help, and we began tossing around ideas.

My grad students Yan Tong and Nathan Liittschwager and I had been working on a new protocol for causal message delivery, based on an idea that I had a while back. We called the protocol Cykas, which stands for “Can you keep a secret?”, and Ayush liked the idea of collaborating on a zine to explain the Cykas protocol!

We quickly realized, though, that to explain the Cykas protocol, we’d have to back up and explain what causal message delivery even was, and say something about the classic approaches to implementing it. So our zine became a bit less about Cykas and a bit more about causal delivery generally. We went through lots of iterations on the writing; one of our goals was to explain concepts precisely without needing to introduce a lot of jargon, and detailed feedback from Julia Evans and Marie LeBlanc Flanagan helped a lot with that.

We had to leave out a lot of things from the zine – for example, we mention logical clocks in passing, but don’t explain how any particular logical clock algorithm works. Even so, this zine ended up almost twice as long as the choreographic programming zine!

Because so many of the ideas we’re discussing are quite old, I ended up going back to primary sources many times, sometimes learning new things myself in the process. There’s a lot of enlightenment to be found in dusty old papers from the last century (but you probably already knew I felt that way).

Working with Ayush on this zine has been an absolute pleasure. Ayush did all the illustrations, and we collaborated on the text. We sweated every detail – I think we went through eleven drafts. Ayush was also new to page layout software, but learned the ins and outs of it just for this project!

Happily, just as we were wrapping this project up, the Cykas paper was accepted for presentation at the PaPoC workshop at EuroSys this year, and I’ll be presenting it there in just a couple weeks! I’m planning to use a lot of the art from the zine in my talk, and I’ll hand out printed zines, too.

Working on zines these last couple of years has been very rewarding. I’ve handed out lots of copies of our choreographic programming zine at conferences, and I’ve gotten emails from people around the world who have printed out copies and handed them out or left them for folks to find, anywhere they think the zine might find an audience. I hope that happens with this new zine, too! Zines are meant to be printed and shared physically. If you like our zine, I would love for you to print one and leave it someplace where someone else will pick it up.

Last month, I was thrilled to have the chance to give a colloquium talk, “Interpreters everywhere!”, at the Indiana University Computer Science Colloquium!

This talk wouldn’t exist if it weren’t for my amazing students. In fact, some parts of it are directly ripped off from talks that my students Gan Shen and Jonathan Castello have given previously on our work: check out Gan’s talk on HasChor from ICFP 2023 and Jonathan’s talk on causal separation diagrams from OOPSLA 2024. It was shortly after Jonathan’s OOPSLA talk in 2024 that I realized that those two projects, which I hadn’t really thought of as having much in common, were really both about interpretation.

So a year later, when I was invited to give a talk at IU – which was the very place where I got hooked on PL via interpreters, back in 2008 when I started grad school – the choice of what to talk about was clear! The rest of this post is more or less a transcript of my talk, not including the Q&A at the end or the lovely introduction by Carlo Angiuli. Those parts, however, are included in the video recording, which you can find on YouTube if you’re interested!

Introduction

I’m so happy to be giving this talk, so thank you, Carlo, for hosting, and for that lovely introduction. I am going to talk about research, but this is much more than just a routine research talk; there is personal significance for me to be giving this particular talk to this particular audience, and I am only sorry that I couldn’t be there in person to visit Bloomington, where it’s so beautiful in the fall.

I’m going to begin, as I so often do, with a little bit of storytelling to set the stage. And the story has to begin with Dan.

I was a PhD student here at IU from 2008 to 2014, and when I arrived in 2008, I took Dan Friedman’s programming languages course, which was fondly known as “Intro to Dan”. In this course, you learn about what programming languages are made of by writing interpreters. So that was how my PhD began, and it was how I got hooked on programming languages as a field.

I was at Indiana for six years doing a PL PhD, and that journey involved a lot of twists and turns that would be enough for a whole other talk. But, long story short, eventually I was working with my advisor, Ryan, on programming language abstractions for writing shared-memory deterministic concurrent programs. And we published some papers about this line of work, using what we called monotonic data structures.

And it was all about shared memory – or so I thought. But then, in the last year or so of my PhD, people who were interested in distributed computing – so, specifically not shared memory – tracked me down and said, “Hey, your work seems to have a lot to do with our work. You really ought to read our work.”

As an example of that, here’s an email I got in 2013 from Marc Shapiro. He’s a well-known distributed systems researcher, and he’s one of the inventors of something called conflict-free replicated data types, or CRDTs, which are data structures that are used in distributed systems to ensure fault tolerance and high availability. So I got this email from Marc near the end of my PhD, and you don’t have to read this, but this is essentially pointing out that I ought to be paying attention to his and his collaborators’ work on CRDTs, ‘cause it had a lot to do with my work. And it turned out, of course, they were right.

Of course, to make sense of CRDTs, I had to do some background reading on distributed systems, and one thing kind of led to another, and, you know, when I started looking at the papers that these folks were recommending to me, it was kind of a revelation for me, since up until then, I had only really paid attention to programming languages as a subfield, and I didn’t really look beyond PL research to consider everything else out there.

But once I did finally look beyond PL, I realized: Wait a second! Distributed systems are actually fascinating! And the field of distributed computing is something that I had a lot to learn from. Not only is it immediately practically relevant to our work and our lives, but it’s also full of profound and beautiful results. And so that’s when I really began to study distributed systems.

Of course, I haven’t stopped being a PL person; PL is still my research home. But for these last, you know, ten to fifteen years, I’ve attempted to study distributed systems from a PL person’s point of view. I was going pretty slowly at first, but this learning process accelerated quite a bit when I got a job at UC Santa Cruz in 2018, and I was suddenly expected to teach distributed systems courses, so at that point it really meant I couldn’t fake it anymore; I had to actually deeply understand something about distributed systems, instead of being a dilettante like I had been up until then. And that in turn influenced what research problems I was interested in. So, these last several years, that’s mostly where my mind has been, research-wise, and my students and I have been going around sneaking distributed systems papers into PL conferences. These papers listed here are a few examples from the last six years, a couple of which I’ll say more about later.

But finally, then, after many years of this, at some point recently I had another revelation. And this one is not going to come as a surprise, you know, to someone like Dan, or really to any of the people here who are part of the Dan Friedman intellectual tradition, which I like to call the Dan-aspora – and of course that includes a lot of you.

And that revelation, of course, was that it was actually about interpreters the whole time! So, despite having been on this sort of long side quest into distributed computing all these years, it turned out that a lot of what my students and I had been doing all this time was still all about interpreters and interpretation.

So, you know – oops.

So in the rest of this talk, I’m going to discuss a couple of our group’s projects that exemplify this realization that I had. And both of these projects are about distributed systems, but I’m going to talk about them through the lens of interpreters. So of course this obligates us to try to answer this question of “What is an interpreter?”

So by the way, I would like this to be interactive if possible, so, you know, for those of you who are on Zoom, feel free to put peanut gallery comments in the chat. They won’t be a distraction to me; in fact, I enjoy it. So I’m interested in people’s takes on, you know, what exactly is an interpreter.

So, what exactly is an interpreter? Well, first let’s see what the dictionary says. And this is actually a shout out to Ken Shan, who, when I asked on Mastodon what an interpreter is, he helpfully sent me this dictionary definition, which is “someone or something that interprets”.

Well, okay, “thanks”. That’s not actually very helpful at all.

But there’s another definition that’s more computing-specific! Let’s see what that one says. There are actually two definitions here. One is “a machine that prints on punch cards the symbols recorded in them by perforations”. Hmm, okay. And the other is “a computer program that executes each of a set of high-level instructions before going to the next instruction”.

Okay, well, “you tried”. I think this definition is pretty bad also. I think we can do much better than this!

Okay, so how am I gonna define what an interpreter is? So, for the purposes of this talk I’m going to say that an interpreter is something that takes syntax and produces semantics.

I like the generality of this definition. It lets us plug in domain-specific notions of “syntax” and “semantics” for whatever domain we care about. And it doesn’t even have to be computing-specific. For example – and this analogy is due to my friend CF – we can think of a choir as an interpreter. I’m a choral singer myself, and this analogy makes a lot of sense to me. It’s the choir’s job to interpret a musical score – usually aided by a director, who, you know, for the purpose of this analogy, we can think of the director as part of the choir – it’s their job to interpret the score and ultimately produce some audible music.

In computing, we might think of an interpreter as something that takes a program and produces a value. I’m using the word “value” here, but I’m using it pretty loosely, because that sounds very pure and like there aren’t any side effects, but a program might well have some sort of effect on the world. I’m not even going to attempt to define “program” here, except to say that both this notion of “program” and this notion of “value” might be domain-specific.

I’ll also point out that the value you produce here might even itself be a program! In which case, what is this last arrow on this slide? Well, now it’s actually a compiler, right? Because you’re taking a program and you’re producing a program. So, you know, at risk of annoying Jeremy and the other compiler folks here, I’m going to argue that, for the purposes of this talk, a compiler can be thought of as just a special case of an interpreter. And I would also argue that every programming language is “interpreted”, because sooner or later your code will be executed by the CPU, and a CPU is itself an interpreter. So it’s interpreters all the way down.

And there’s one last really important thing that I want to mention about what “interpretation” means. So – if you’ll continue to indulge me with this choir analogy – so, a music score for a choir is typically going to have different parts, right, that different people sing. So, if we say that syntax is interpretable, then that usually is going to connote something about the form that that syntax takes. In particular, it’ll say something about how the interpretation of a given input has to be determined by the interpretations of its subcomponents, and the result you get is compositional. To be able to do this, there has to be an obvious way to break down the input into its subcomponents and put them back together. In other words, it has to be inductively structured data – you know, like an AST.

So what I want to do next is dig into a couple of specific places where this idea of interpretation seems to have arisen in my own work in these last several years.

I’m going to focus on two projects from that list that I gave earlier, and those are library-level choreographic programming and causal separation diagrams. I’m going to talk about both of these things, and I won’t really have time to do more than just scratch the surface of either of them, but I’m really happy to dig into the details in Q&A, or chat with folks later. So, let’s jump in, and let’s talk about library-level choreographic programming first.

Library-level choreographic programming

Okay, so let’s talk distributed systems!

In the world of distributed computing, we’re usually concerned with message passing. The idea here is that you have some independent nodes that communicate with each other via a network, and they do it by sending and receiving some kind of messages. They don’t share memory, so the only way for them to coordinate with each other is by passing messages. And you might be able to imagine having some sort of so-called “distributed shared memory” as an abstraction on top of this, but under the hood, it’s ultimately all message passing.

So, let’s suppose that our independent nodes are Alice and Carol. And there’s typically some kind of, you know, global behavior that we want here. And Alice and Carol have to together accomplish that, but they have to do it by taking only local actions, so the only thing that either of them can do is send messages, or receive messages, or take internal actions.

So, if we want to run a really, really simple protocol in which Alice sends a request to Carol and Carol responds to Alice, how do we program that?

Well, we can assume for now that we have some sort of send and recv functions that actually implement the message transport somehow, so it might be TCP, it might be HTTP, it might be pigeons flying around. Let’s not worry about the details of how the transport layer is implemented; let’s just think about what Alice and Carol have to do assuming it exists.

So, for this protocol, Alice would run this node-local program here on the left, and it might look like this: send a request to Carol, and then wait to receive a response from Carol, which gets stored in this variable here.

Meanwhile, Carol is running her own node-local program, which might look like: receive request from Alice and store it in this variable request, then do something to handle the request, and finally send a response.

So this is just about the simplest distributed program that I could could conceive of, but even in this really simple program, notice how Alice and Carol are utterly dependent on each other to faithfully follow the protocol. So, for instance, if Carol neglected to call recv over here, now that’s become Alice’s problem. So Alice will wait forever to get a response, or what she might do is time out and report an error, depending on how send is implemented. So in general, in a distributed system, nodes have to execute messages in this very careful dance where a message sent from a node has to be expected by some recipient, and vice versa. So if somebody is running buggy code, then things go wrong for somebody else.

And it only gets more complicated if we add nodes. Let’s say that Alice is sending Carol a request, and then Carol is supposed to pass the request along to Bob, and then get an acknowledgment from Bob, and finally respond to Alice to acknowledge her request. This is the sort of pattern that you might see, for instance, in primary-backup replication, where – let’s say Alice is the client, Carol is the primary, and Carol gets a request from Alice which she has to pass on to Bob, Bob has to ack Carol, and Carol has to ack the client. In this scenario, Alice may not even know that Bob exists. But nevertheless, if Bob is misprogrammed, then that could mean bad news for Alice.

In fact this, example calls to mind this wonderful quote from Leslie Lamport in which he defines a distributed system as “a system in which the failure of a computer that you didn’t even know existed can render your own computer unusable.”

So the challenge, then, for programmers is to try to reason about the behavior of this distributed system – the implicit global behavior of this system – while writing the explicit local programs – which are just sends and receives and internal actions – that actually run on the nodes.

So, this brings us to choreographic programming. And the idea of choreographic programming is: let’s make that implicit global behavior actually explicit in the code! In choreographic programming, we don’t write the local programs at all. Instead, we write a single, global program that’s called a choreography. And then we generate a collection of local programs, one for every node, from the choreography, via a technique called endpoint projection.

So what we have on the left here is a choreography that expresses the protocol that we talked about earlier. So, every choreographic programming language is going to have some sort of operator like this highlighted squiggle-arrow ~> here. And this is usually pronounced “comm”, because it denotes communication between two parties.

So, looking at this first line here in the choreography, a ~> expression is going to express a both send and a receive at once. And what this means is that Alice is going to compute this value request, communicates it to Carol, Carol receives it and stores it on her end in the variable x. When this choreographic program gets projected, every time you have an occurrence of Alice on the left-hand side of a ~>, it’s going to turn into a send call on Alice’s node, and every time you have an occurrence of Carol on the right-hand side, that’s going to turn into a recv on Carol’s node.

Thanks to this way of writing code, as long as our endpoint projection is correct, we can rule out the possibility of a mismatched send and receive, and we can therefore rule out a certain kind of bugs that could occur in our collection of local programs that we end up with. In a nutshell, that’s the benefit of choreographic programming.

I do want to acknowledge one of the elephants in the room, which is that with what we’ve shown so far, choreographic programming per se doesn’t actually do anything to help us if one of these nodes should crash, or if one of these messages should be lost. So, those fault tolerance problems were present in the non-choreographic version of the code, and they’re still present here. So choreographic programming doesn’t do anything to fix that as such.

What it does do is rule out programming errors that stem from a programmer not calling send where they should or not calling recv where they should. In a simple program like this, that might not seem like such a big deal. But once more parties are involved, it becomes less simple, and it’s in that multi-party setting where choreographies really shine. So next let’s look at a setting with three participants and with some more interesting control flow.

OK, so this is a slightly more interesting protocol. Suppose that Alice wants to interact with Carol, but Bob stops her to check her credentials first. So, this example is kind of like a sign-on through an third-party authentication service.

And by the way, this example is straight from the choreographic programming zine that my student Ali and I wrote last year, which you can get from my website if you want. In the zine it’s that Alice wants to go to Carol’s birthday party but she’s stopped by the bouncer Bob.

In this protocol, Alice has to have her credentials verified by Bob before she can interact with Carol. So, Alice sends those credentials to Bob. Bob runs this check function on Alice’s communicated credentials, and then, depending on the outcome of that, Alice will either get an access token from Carol or not. So this diagram represents two different ways that an execution might go.

So, how do we express this in a choreography? Well, in a choreography, we can have conditionals at the choreography level, and here’s what that looks like. So, on the first line, here’s our squiggle-arrow again. And this notation Alice.credentials ~> Bob.authRequest means Alice is computing something called “credentials” and then sending it to Bob, who receives it and then stores it on his end in this variable called “authRequest”.

And then we have a conditional. So, the conditional check takes place locally on Bob’s node. And then, depending on which branch we take, either Bob communicates “Success” to Carol, who then communicates the token to Alice, or Bob communicates “Failure” to Carol, and then Carol tells Alice that she can’t have the token.

So what I think is useful to point out about this execution is that even though the execution is spread out across these three different parties – so this is a distributed execution – if we think about the execution globally, this is actually a sequential program in which steps happen one after the other. And we can see that from reading the choreography; the choreography just looks like straight-line code. In fact, the choreography looks remarkably similar to our informal diagram that we drew. So, if we were to write this code as a traditional distributed program, which is really three programs running on the three participants, then the control flow wouldn’t be as obvious. So having it as a choreography actually helps the readability of the code as well.

OK, so to actually run this thing, we need to do endpoint projection on it. So, endpoint projection will take this choreography and it’ll project it to versions running on Alice, Bob, and Carol, and this is done automatically by the choreographic language implementation. And I’ve written some pseudocode to give an idea of what the projected code might look like. And notice, like I said, in this projected code, the control flow isn’t as clear. You might have to stare at it for a bit to figure out what’s supposed to happen first, what’s supposed to happen second. So choreographies give us this readability advantage.

There’s some stuff that I’m leaving out here. One important side note here is that when you do endpoint projection, if the choreography had a conditional like this, then the parties that are involved need to be told what branch to take. And this is called the “knowledge-of-choice” problem. Different choreographic languages have different ways of dealing with this. For instance, if I hadn’t had code in my projected code that commmunicates the outcome – or if I didn’t have code in my choreography, rather, that communicates the outcome of this check(authRequest) call, then some choreographic languages would then complain that the choreography is what we call “unprojectable”. And other languages would just insert the necessary communication code for you. So that’s all an interesting problem in its own right, and if you’re interested in knowing more about that, then I’m happy to talk more about it later.

OK, so now you know what choreographic programming is. So, we didn’t invent any of this stuff; choreographies have been around for a long time. Dating back to the early 2000s, there was something called the World Wide Web Consortium’s Web Services Choreography Working Group, and they developed a draft specification for a language called WS-CDL, which stood for Web Services Choreography Description Language. However, this wasn’t intended to be executable; it was only a specification language – you couldn’t actually run these things.

So, fast forward to 2013, when there was a language called Chor developed by Marco Carbone and Fabrizio Montesi. And this pioneered the idea of an executable choreographic programming language that used endpoint projection to compile choreographies to these runnable node-local programs.

Then in 2020, Fabrizio Montesi teamed up with Saverio Giallorenzo and Marco Peresotti to create the Choral programming language. And Choral is intended to be useful for realistic programming, and it’s notable for how it uses mainstream object-oriented programming abstractions, so it’s designed to be familiar to, say, Java programmers. And the Choral compiler projects choreographies to executable Java code.

Then, in 2022, Andrew Hirsch and Deepak Garg created a choreographic language called Pirouette, which combined choreographic programming with higher-order functional programming. This paper made a splash in the functional programming research community, and it won a Distinguished Paper Award at POPL that year, and this is how my students and I found out about choreographic programming for the first time. And this paper, by the way, is also notable for its mechanized proof of deadlock freedom.

So, my student Gan Shen read the Pirouette paper and decided he wanted to try implementing a choregraphic language himself. And so, being who he is, the approach that seemed obvious to him was to do it as an embedded domain-specific language in the form of a Haskell library. And the idea is really straightforward, and what’s funny about this is that Gan wasn’t even trying to do something novel – he just wanted to learn about choreographies. But it turned out, to our surprise, that this idea of implementing a choreographic language purely as a library had not been done before. And this appeared at ICFP ‘23, where it also won a Distinguished Paper Award. (So for a couple years in there, every paper about choreographic programming in PACMPL was getting a Distinguished Paper Award – sadly, no longer true.)

So let’s dig in a little bit and talk about HasChor and how it works.

So I’m gonna contrast this with the traditional approach to choreographic programming, which is exemplified here by Choral. In Choral, you write a choreography in the standalone Choral language and you compile it to executable endpoint code using a standalone compiler. So Choral compiles to Java, and then you can run those Java programs using the usual Java toolchain. And this all works fine, but it means that you need this purpose-built language and this purpose-built compiler.

In HasChor, on the other hand – and this is our framework – choreographies are expressed as programs in an existing host language – in this case it’s Haskell – and the choreographic language constructs and endpoint projection are all implemented entirely in this host-language library, so there’s no additional compiler support needed, no additional runtime support needed beyond what the host language can already do.

So in particular, our choreographic language is implemented in Haskell as a DSL using something called a freer monad, which separates the interface and implementation of effectful computations. So by itself, this language doesn’t assign any meaning to choreographic operators like that ~> that I was talking about before. Instead, it just accumulates them as this big term, and then we dynamically interpret that term, based on the location where the code’s being run. So, for instance, that ~> operator: if you’re a sender, that gets interpreted as send, if you’re a recipient, it gets interpreted as recv, and if you’re anyone else, then it’s a no-op.

All the usual benefits of embedded DSLs apply here. So, because these programs in HasChor are really just Haskell programs, that means that a HasChor programmer can take advantage of the whole Haskell ecosystem. They can use their existing Haskell tools for development and debugging, they can use other Haskell libraries, and they can compile it just like any other Haskell program. Whereas, for something like Choral, it’s a whole new language, right? You might not have any tooling unless the developers bother to implement it.

And there’s one other plus side, I think, to this embedded DSL approach, which is that it makes it easier to integrate choreographies into bigger non-choreographic systems, so there’s no need to change languages just to implement certain pieces as choreographies. And I think this is really important, because while choreographic programming may be a good fit for certain components of a program, there might be other parts of the program where trying to fit it into that choreographic paradigm just doesn’t make sense. So maybe you have a program where almost all of the code happens locally, but maybe there’s like a short-lived network interaction, just to do authentication or something. So then, you know, it wouldn’t really make sense to have to write everything in a choreographic language just so you could get the benefit of choreographies for that one little piece. So that’s an argument in favor of this library-level approach.

And one of the consequences of this is that endpoint projection actually happens dynamically, at run time. So let’s take a look at the type of the endpoint projection function in HasChor, and I hope to convince you that it’s really just an interpreter. I promise you that this is the only line of Haskell code that I’ll make you look at in this whole talk.

So, endpoint projection is a function that takes two arguments. The first argument is this Choreo thingie here, which is a choreography. So, endpoint projection takes one of these choreographies, and the second argument it takes is a location, which is the place we want to project the choreography to, so, like, Alice or Bob.

And endpoint projection returns something called a Network, which you can think of as a low-level program in terms of sends and recvs that’s been specialized to the location you gave as an argument.

So for the Haskell enthusiasts here, both Choreo and Network are freer monads. But you should think of them both as just being programs. And these choreographic operators that are in Choreo programs all get interpreted to things like send, recv, and broadcast in the Network programs. So Choreo gives us a syntax. On the Network side, we have – I’ve put “semantics” in quotes here, because this isn’t actually semantics, it’s still just syntax, and then that will get dynamically interpreted to the actual meaning of send and recv and so forth. The actual meaning of send and recv and so forth is going to be supplied by a network backend, and HasChor comes with two of those that you can choose between. There’s an HTTP backend which uses HTTP for the network transport, and there’s a local backend which implements these send and recv functions as communication among threads on a single machine. So that’s endpoint projection: it’s just an interpreter!

So, returning to our timeline of choreographic programming, it’s really exciting how since HasChor came out in 2023, a bunch more choreographic languages-as-libraries have popped up. So there’s a bunch more new choreographic programming libraries in these last two years. Some of them are from our group – so, MultiChor is a successor to HasChor, ChoRus is a choreographic programming library for Rust, ChoreoTS is a choreographic programming library for TypeScript – but what’s even more exciting to me is that a bunch of these are not from our group. So there’s ChorCaml for OCaml, there’s Chorex for Elixir, there’s Klor for Clojure, there Choret for Racket, and there’s UniChorn, which is for a distributed programming language called Unison. So all of these are doing dynamic endpoint projection, so endpoint projection at run time, just like HasChor, but they all do it using the idioms that make sense in those languages. So, for instance, Choret is built on top of Racket, and in Choret it’s done using macros, which is super cool. So all of these different approaches use the idioms that make sense in the languages that they’re implemented in, and I love that.

All right, and here I’ve just given the GitHub URLs for a couple of our projects. So here’s the HasChor repo and here’s the repo for ChoRus, which again, is our choreographic programming framework for Rust. So feel free to take a look at these and check them out. This is work led by my students Gan Shen and Shun Kashiwa, and then ChoRus was also – the lead author on it was Mako Bates, who is a recent PhD graduate from Joe Near’s group at the University of Vermont.

Okay! So, that’s it for the first line of work I wanted to talk about, on library-level choreographic programming.

Causal separation diagrams

And now I want to talk about causal separation diagrams. So, let’s talk diagrams!

So, people who work on concurrent and distributed programming been using diagrams like these – I call them Lamport diagrams, but they’re also known as sequence diagrams and time diagrams and a bunch of other names – people have been using diagrams like these since – at least since the 1970s, as a way to try to wrap our heads around how concurrent and distributed systems work. I’ve been using them throughout this talk. And they’re pretty intuitive, you know? I didn’t have to explain what these diagrams mean. And you might have drawn one yourself on a whiteboard recently.

These diagrams depict the events of interest in a system – usually things like when message are sent or received – and the relationships between those events across space and time. And these diagrams are so intuitive that we see them at all levels of academia and industry.

But they are just pictures, right? They’re not formal objects – but they could be formal objects!

So, if we want to reason formally about executions like the one that’s shown here, we need a formal model of executions. So, let’s talk about how to do that. And I’ll put the diagram on the left here, and this textual formalism on the right, but these are really expressing the same information.

So the first thing we would need is a collection of processes, right? These are modeling whatever locations are participating in the system.

And then, every process is going to have a sequence consisting of the events that occurred on it. And events could be message sends, or they could be message receives, or they could be events that are internal to a process. So we have a sequence of events on each process that’s totally ordered.

And then, last, we’re going to have pairs of events that comprise “messages”, which is where information propagates from one place to another. So here, for instance, \(a_1\) would be a local event on this process \(P_1\), \(a_2\) would be a message send event, and the message is being sent to \(P_2\), where the receive event is \(a_5\).

So what I’m showing here is a completely standard way to formalize executions, and it get used all the time, with good reason. But it does have some pitfalls. So, what are some of the problems with doing it this way?

One issue is that this representation, doesn’t stop you from representing something that’s actually physically impossible, like a causal loop. So here, \(a_2\) is the send event for this message, \(a_5\) is the receive event, and then later on process 2, we have a send event for a message that’s being sent backward in time, back to \(P_1\). So this is an execution that couldn’t actually physically happen, and the structure of our data doesn’t really help us avoid this situation. The formalism will still let us write down this execution that couldn’t actually occur, and you would need to do some additional checking to make sure that your data is self-consistent.

The other problem is that this representation doesn’t stop you from representing what are called inconsistent cuts.

So, a consistent cut in an execution like this is something like this blue line with a happy face here. It’s separating the events of the execution into a clear past and a clear future. So, here, the “past” is what’s above this blue line, and the “future” is below it. And if an event is on the “past” side of the cut, then if it’s a consistent cut, then everything that’s causally before that event is also on the “past” side of the cut. And this blue cut is in fact a consistent cut.

An inconsistent cut, like the one represented by the red line here, fails to have that property. So here, for instance, we have this event \(a_5\), which is on the past side of this cut – but \(a_5\) represents the reception of a message that was sent here at \(a_2\), which is actually on the future side of the cut. So \(a_2\) should causally precede \(a_5\), but \(a_2\) is on the future side of the cut.

So the traditional model doesn’t help us avoid inconsistent cuts. And so, if I just take a prefix like this of the events on each process, well, it might be a consistent cut or it might be an inconsistent cut. And the problem is that there’s no connection between the processes that we’re splitting into past and future, and the messages we need to respect.

So you might have heard of this famous software development dictum “make illegal states unrepresentable”, which I think is due to Yaron Minsky. As my student Jonathan put it, this way of representing executions makes illegal states all too representable.

Okay, so what do we do about this? What should we do instead?

To get a better idea of what’s problematic about the traditional approach to representing executions, let’s take a closer look at it. So here I’ve written down the same execution we were looking at before. I’ve turned the diagram on its side, and kind of flipped it around, and I’ve removed the labels on events. But it’s the same execution as before; it’s got the same structure.

The only difference is that I’ve added some additional dotted gray and dashed blue lines to this diagram, which make the structure of the execution more explicit. So, in this traditional approach, the top-level structure of this execution is this collection of processes, so the first thing we have to do is visually separate these processes from each other. And that’s what these dotted gray lines do. And we can think of them as spatial boundaries between the processes.

And next, each of these individual processes has a sequence of events in time. And we can make that explicit too, by adding these dashed blue lines as temporal boundaries between events.

Unfortunately, we cannot really do the same thing with messages. Because we made the order of events within a process our top priority, messages are kind of a different kind of entity. But notice how these message arrows always seem to cross these gray “spatial” boundaries, which run horizontally. They cross those rather than crossing the blue “temporal” boundaries, which run vertically. So these process-local edges that cross over the dashed blue lines are inherently causally ordered by the structure of the data, but the edges that cross over the dotted spatial boundaries between processes are not inherently causally ordered by the structure of the data. And that is what makes it possible to accidentally construct an inconsistent cut.

So, this happened because we prioritized the spatial boundaries first, instead of prioritizing the temporal boundaries. What would happen if we did it the other way around? What would happen if we laid down the temporal boundaries first, and then the spatial ones?

That’s exactly what our approach does. So here’s that same execution again, but now represented using one of our diagrams, which we call “causal separation diagrams”. So, it’s the same execution, but represented in a different way.

First, we’re laying down enough consistent cuts to separate every event. That’s what these vertical dashed blue lines are. So, instead of splitting up by processes first, we’re splitting up this execution into these global time steps, where by “time” I mean logical time. And then, within each of these global time steps, we can add these spatial boundaries between each distinct location.

And we end up with this different way of decomposing our diagram. So the original way of decomposing it, we had this structure that consisted of these three separated sequences of events. In our new decomposition, we have a single sequence, not of events but of “global steps”. And then those global steps, which are these columns here, delimited by these dashed blue lines, those are each made up of “local steps” delimited by the spatial boundaries.

So here we’ve got four big global steps arranged from left to right, separated by the blue dashed lines, and then every global step happens to contain three local steps, separated by these gray dotted lines.

So, this choice, to prioritize the temporal boundaries over the spatial boundaries, is the fundamental difference between our approach – CSDs – and the traditional model. And everything else is just a consequence of that. And I’ve been saying “temporal” boundaries, but I could also just as well have called them causal boundaries, because this potential causality here is following the flow of time. Hence the name “causal separation diagrams”.

What’s most interesting here is that both messages and processes now evolve over causal boundaries. Information never crosses directly across a spatial boundary. And as a consequence of that, a diagram that can be decomposed this way necessarily has no causal loops. In other words, if we can construct diagrams this way with a CSD, then they are necessarily going to be causal by construction. So we have made illegal states unrepresentable.

Here are all the different kinds of local steps that we can build diagrams out of. In the first two here, a tick is just a local event on a process, and a noop is the absence of an event.

These last two – swap and assoc here – they don’t model any actual events. Instead, they just allow us to rearrange the wires through the diagram so that processes can communicate with more than just their immediate neighbors. You can think of these as sort of like structural rules in a logic.

And the middle two – fork and join – these are modeling the two halves of a traditional message. But unlike in a traditional message, we have both the process and the message state that are coming out the right-hand side, rather than having the message go out the top or bottom.

So, in fact, our model doesn’t distinguish process state from message state at all! Nothing prevents a so-called “process” from joining state with another process, or a local event from occurring on a message. So we’re referring to these inputs and outputs uniformly not by “processes” or “messages”, but by “sites”. A site is just a place where state can exist. This was my student Jonathan’s innovation, and it took me a while to get my head around treating messages and processes as the same thing, but it actually makes sense to me now. So a process sending a message is just a site forking off a piece of its state out into the world as a new site, and a process receiving a message is just two sites joining together.

So now that we have these tiles, these composable tiles, we can stick them together however we like and get a consistent CSD. And I’ve left it out here for brevity, but each one of these tiles actually has a type, which says how we’re allowed to compose it with other tiles. And we also have combinators for composing local steps into global steps, and for chaining global steps together into an execution. And the type of each tile tells you how it can be composed with other tiles vertically and horizontally. And for the fancy type enthusiasts here: yes, these are dependent types!

So, okay, so what does all this have to do with interpreters, which is the topic of this talk? So, earlier, when we were talking about what interpretation meant, I said that if we say that a syntax is interpretable, that usually means that the interpretation of a given input is determined by the interpretations of its subcomponents. And to do that, we need to have an obvious way to break down the input into subcomponents and to put it back together. The “obvious way” to break things down and put them back together is what we call an induction principle.

So, for that traditional formalization of executions that I showed first, we unfortunately don’t have a nice induction principle for the thing on the left here; we just have a set of processes and a set of messages, and the structure of the data doesn’t tell us how we’re supposed to break things down and put them back together. So executions that are represented in this traditional way on the left are not particularly amenable to interpretation – not if we want to work in a tool that encourages us to inductively define data structures, especially like a mechanized proof assistant.

But on the other hand, executions that are represented as causal separation diagrams come with a lovely induction principle, since they’re actually just lists of global steps. So, to take a CSD apart, you can just peel off one global step at a time; to put it back together you can just glue on one global step at a time. And this makes CSDs amenable to interpretation.

So, CSDs give us a formal, graphical, inductively defined syntax for representing concurrent executions, and that’s something that we can straightforwardly write interpreters for. So that’s exactly what we do. In our paper we talk about three ways to interpret CSDs – that is, three ways of giving CSDs a semantics!

The first of these is an interpretation of CSDs into what we call causal paths. Causal paths are nothing but a proof-relevant analogue of the classic Lamport happens-before relation. So, instead of just saying that two events are causally related or aren’t causally related, we can interpret a CSD into a dependent type of the causal paths through a diagram, and these paths give evidence of the causal relationship between events.

The second way that we interpret CSDs is into logical clock functions, which assign an event to its corresponding logical timestamp. So there are a lot of different kinds of logical clocks that get used in distributed system implementations: Lamport clocks, vector clocks, matrix clocks – our interpretation is parametric in a choice of clock implementation, so you can instantiate the same machinery over many logical clocks, and we’ve done that for a bunch of different flavors of clocks.

And the third way that we give to interpret CSDs is into proofs that clocks respect causal paths. So a logical clock that respects causal paths is a clock that satisfies Lamport’s clock condition, which is the thing that makes a logical clock a logical clock. So using CSDs, we’re able to give a mechanized proof of the clock condition that’s parametric in the choice of clock. This interpretation-based approach to verification of clocks would be really awkward and difficult if we didn’t have this inductive data structure that accounts for causality; but with CSDs, it just kind of falls out naturally.

So, to wrap up this part, I’ll just mention that you can find our proof development on GitHub – this is done in Agda – and my student Jonathan and I are actively looking for more things to use CSDs for, which I’d love to talk with folks about.

Conclusion

Okay, so, we’re almost at the end. So, to sum up: I’ve talked about two lines of work from my research group that turned out to be all about interpreters, all along.

So we talked about library-level choreographic programming, which lets programmers write distributed programs as single, unified programs in their favorite language, and then dynamically project them to multiple endpoints.

And we talked about causal separation diagrams, which are inductively defined data structures designed for elegant mechanized reasoning about happens-before relationships in concurrent executions.

But really, we could sum up these two lines of work as being about interpreters. HasChor is just asking, “What if endpoint projection was an interpreter?” and CSDs are just asking, “What if you could write interpreters for Lamport diagrams?”

So the takeaway I have for you here is: you can’t go wrong by studying how interpreters and interpretation work. And then go study something else, and reap the benefits of applying your knowledge to that new domain.

So that’s all I’ve got, and I want to thank you for your attention!

When did computer scientists start to talk about “simulation” between programs? As of a couple of months ago, the earliest paper I had seen on this topic was Robin Milner’s widely cited IJCAI 1971 paper, “An algebraic definition of simulation between programs”. (That’s the official publisher’s version, but this tech report version seems to have more readable typesetting.)¹

Recently, though, I came across this historical overview of bisimulation by Davide Sangiorgi, published in TOPLAS 2009. Sangiorgi’s paper is mainly about bisimulation, but he discusses simulation as a necessary stepping stone to bisimulation. Sangiorgi, who was Milner’s Ph.D. student, had this to say about Milner’s early work on simulation:

Decisive progress towards bisimulation is made by Milner in the 1970’s. Milner transplants the idea of weak homomorphism into the study of the behavior of programs in a series of papers in the early 1970’s ([Milner 1971a, 1971b, 1970], with Milner [1971a] being a synthesis of the previous two). He studies programs that are sequential, imperative, and that may not terminate. He works on the comparisons among such programs. The aim is to develop techniques for proving the correctness of programs, and for abstracting from irrelevant details so that it is clear when two programs are realizations of the same algorithm. In short, the objective is to understand when and why two programs can be considered “intensionally” equivalent.

To this end, Milner proposes (appropriately adapting it to his setting) the algebraic notion of weak homomorphism that we have described in Section 4.1. He renames weak homomorphism as simulation, a term that better conveys the idea of the application in mind. Although the definition of simulation is still algebraic, Milner now clearly spells out its operational meaning. But perhaps the most important contribution in his papers is the proof technique associated to simulation that he strongly advocates. This technique amounts to exhibiting the set of pairs of related states, and then checking the simulation clauses on each pair. The strength of the technique is precisely the locality of the checks that have to be made, in the sense given to locality in Section 2.1. The technique is proposed to prove not only results of simulation, but also results of input/output correctness for programs, as a simulation between programs implies appropriate relationships on their inputs and outputs.

The Milner [1971a] paper that Sangiorgi refers to is the aforementioned IJCAI ‘71 paper that I had been aware of, but Sangiorgi also cites two slightly older papers, one from 1970 and one from 1971. Both of these are listed in Sangiorgi’s bibliography as being unpublished memos from Milner’s time at Swansea University:

MILNER , R. 1970. A formal notion of simulation between programs. Memo 14, Computers and Logic Resarch Group, University College of Swansea, U.K.

MILNER , R. 1971b. Program simulation: An extended formal notion. Memo 17, Computers and Logic Resarch Group, University College of Swansea, U.K.

I couldn’t find digital versions of either of these old memos online. Milner does also cite them both in his IJCAI ‘71 paper, and he says that the IJCAI paper “is a synthesis of the two, and may be read independently”, so I wasn’t particularly worried about missing any useful science by looking only at the IJCAI ‘71 paper rather than the two older papers.

But we’re not in this just for the usefulness, are we?

I asked around on Mastodon to see who might have access to the two memos, and Jeremy Gibbons came through. The two papers were physically located in the Programming Research Group Archive at the University of Oxford’s Computer Science Library:

The Computer Science Library holds the archive of the Programming Research Group (PRG). It is contained in 240 box-files which hold papers and technical reports produced by PRG members and allied computer scientists between the early 1960s and 1980.

Jeremy kindly contacted the library on my behalf, and heroic librarian Aza Ballard-Whyte located the two papers somewhere in those “240 box-files” and personally scanned and emailed them to me on the other side of the planet. To my amazement, they are handwritten, and they are absolutely gorgeous.

They don’t seem to be on the public internet anywhere. I asked Jeremy if it would be okay to share them, and he said he didn’t think it would be a problem. So without further ado, here they are:

• “A formal notion of simulation between programs”
• “Program simulation: an extended formal notion”

The first paper in particular is a delight. Aside from being in Milner’s lovely handwriting, it also has a few of his own handwritten corrections and comments on it, in red and green ink.

I’ve transcribed the first four paragraphs of the first paper below. I hope you will agree with me that what Milner had to say about what programmers do when writing code, and about how programmers think about their programs, is damn near as true in 2025 as it was in 1970.

Programmers often choose an unnatural representation for their data objects, even when a more natural choice exists in the language they are using. Their reason may be that they do not wish to incur the space/time overheads of the more natural choice of data types, particularly when they only use frequently a subset of the operations available over those types – and when that subset is efficiently carried out in terms of a less obvious choice of data representation.

An example of this is in the storage of clauses in a resolution-based theorem-prover. Clauses are naturally sets of formulae, and a formula is naturally a tree or nested list. But because (i) clauses once formed are not normally alterned or extended, and (ii) the frequent operations on clauses – e.g. unification, substitution – are efficiently done on a string or vector representation, one would not except for pedagogic reasons use for clauses the data types set, list even in a language which had them.

Whatever the reason for choosing an unnatural representation, programmers continue to think in terms of the natural data objects too; it follows that they are aware of the mapping – or whatever it is – that exists between them, however implicitly. Part of the purpose of this paper is to formulate whatever it is explicitly: we show how the real program simulates (in a precise sense) the ideal program that never got written.

Motivation comes from the fact that proving that an ‘unnatural’ program works – a task certainly too hard for complete mechanisation at present except for the most trivial cases – or even expressing what it is supposed to do, appears to involve making the simulation at least partly explicit.

As an example of a program that uses “unnatural” data structures, Milner draws on one of his own even older Swansea memos from 1969 (which I haven’t looked at), appropriately called “The difficulty of verifying a program with unnatural data representation”. The program takes two arrays of characters \(\sigma\) and \(\tau\) and one character argument \(c\), and is supposed to produce a new character array consisting of \(\sigma\) but with all occurrences of \(c\) replaced by \(\tau\). (For instance, if the arguments were "foo", "bar", and 'o', we would get "fbarbar".)

Milner observes that if one writes this program without the help of ‘natural’ data structures, determining that the program is correct involves a fiddly correctness criterion defined in terms of a metafunction he calls “seq”. This example, he says, illustrates how “program verification is most naturally done in terms of the natural data objects”:

If the programmer has in mind, while writing this program, an ‘ideal’ program with a similar flowchart and with string variables, then the values assumed by the latter will roughly correspond to the values of the ‘seq(…)` subexpressions in the assertions. In fact one may hope for a kind of homomorphism from the statespace of the real program to that of the ideal program, since the latter’s variables take values which are functions of those in the former.

What Milner is suggesting here is that the real program, with its “unnatural” data representation, is in some kind of implicit correspondence with some ideal program in the programmer’s head, which has a “natural” data representation – in particular, lists, which, if their elements are characters, are also known as strings. (When it comes to data types, the humble string might not seem like a particularly high level of abstraction. But, remember, this was 1970! The C programming language, for example, did not exist yet.)

Milner then goes on to formalize what such correspondences between programs – which he, and generations of computer scientists since, have called simulations – look like when they are made explicit. This is the meat of the paper, and I won’t go into detail about it here. Instead, I want to focus on this absolutely gorgeous hand-drawn figure. Such diagrams are ubiquitous now in program verification textbooks, but this might have been one of the first times that someone drew one!

Here, the “real” program \(A'\) (on the right) simulates the “ideal” program \(A\) (on the left) – or, if you like, the “ideal” program \(A\) is simulated by the “real” program \(A'\)). The key thing to notice is how the two programs represent data objects differently. For instance, in the “ideal” program on the left, we see the tell-tale presence of “hd” and “tl”, which are list operations that respectively return the first element of a list and all but the first element of a list (or the first character of a string and all but the first character of a string, if you prefer). The “real” program on the right, \(A'\), does not use those list operations, and is an example of a program in which “the natural data objects were not directly represented”, in Milner’s words. But, once we know that \(A'\) simulates \(A\), then if \(A\) is correct, we know that \(A'\) is correct. Milner concludes section 4 of the paper: “total correctness of \(A\) implies the same for \(A'\)”. Although the example in this 1970 paper is just a toy, it illustrates a powerful idea that lies at the heart of industrial-strength verification efforts based on refinement proofs, like the seL4 OS kernel.

I sent Aza a thank-you postcard with a Santa Cruz beach vista on it.

The course was a blast! The idea was to write an interpreter for Lox, the toy language from Bob Nystrom’s Crafting Interpreters book. The book already presents a complete Lox interpreter in Java, but we were doing our own thing in Rust, and I pretty quickly stopped following the book’s code since it was very different from what I was trying to do in Rust. If you’re curious what I ended up with, my code is now public. It’s incomplete – I only got as far as section 8.1 of the book – but it runs and does stuff; give cargo run a whirl! If a course like this sounds fun to you, consider taking one of Dave’s various upcoming courses.

I posted lots of thoughts about the course on Mastodon after each day ended. Here are all of those, cleaned up and collected in one place.

Day 1

• We’re only on lexing so far. Dave mentioned that it’s kind of a bummer that the course has to start with tedious string processing stuff. It wouldn’t have to be that way! We could have gone back to front! But that’s the way the Nystrom book is written, and we’re following the book.
• I’m doing more talking than anyone else other than Dave. I wish other people would speak up more. I have no idea how far along they are, or if this is hard for them or easy for them or what.
• The Nystrom book uses Java as its implementation language. Rust is really different from Java along at least two axes: low-level memory layout concerns, and, uh, “object-orientedness”. It is kind of fun trying to figure out how to port the Java code to Rust while navigating both of those at once.
• We are doing quite a lot of talking about error handling. That’s probably a good thing!
• I find the ? thing for error handling in Rust to be rather mysterious so far, and I’d much rather write explicit matches on Results. I can always refactor later once I figure out what I’m doing. (Perhaps it’s not really different from a typical Haskell pattern for error chaining, as seen when programming with Maybe or Either, and so it ought to be familiar to me. But hey, I never claimed to be good at Haskell either.)
• We talked a lot today about how slicing strings doesn’t respect character widths. Someone had a cute example of slicing a ZWJ’d emoji in half and getting one of the constituent emoji.
• I don’t really know if I am writing idiomatic Rust. I don’t even know if anyone in the class can tell me whether I’m writing idiomatic Rust.
• I spent quite a while today trying to figure out how to implement Display on things, then trying to figure out if I could derive Display, all kind of needlessly.
• Dave mentioned that he didn’t want people to get hung up on fiddly details of Rust and thus lose sight of the big picture. On the one hand, I already feel very comfortable with the big picture of interpreters; fiddly details of Rust are exactly what I’m here to learn! On the other hand, I do want to actually “finish” the project by the end of the week, which will probably require sacrificing some attention to detail. We’ll see how it goes.

Day 2

• We talked a bunch about move semantics today. It’s funny, but the time I’ve spent thinking about choreographic programming – where all data and computation is located somewhere, and it moves around when communication occurs – actually seems like it could be helpful for reasoning about data movement in Rust.
• I’m worried about having enough time to write code. This course is really making obvious what a weird silo of knowledge I have as an academic PL person! I could have any number of deep conversations about PL concepts in the abstract, but I’m super slow at actually writing code; I don’t have the muscle memory for anything, I have to look every little thing up, and I usually know enough to know my code is inelegant, but not enough to know how to fix it.
• That said, I think I might waste time preemptively looking things up, when in Rust I could actually just try stuff and then let error messages tell me what to do. For example, it is really slick how if you don’t know, say, what functions you need to implement for a trait, you can just write impl Trait for Type { } (with the actual name of the trait and the type, of course!), and the compiler will tell you what’s missing.
• From the Nystrom book: “In Lox, as in most programming languages, the rules of that grammar are simple enough for the language to be classified a regular language.” Hmm, really? Are “most programming languages” regular languages? I don’t think so.¹
• I had to derive PartialEq on a bunch of my types so that I could write tests with assert_eq!. I was curious what “partial” meant. (In Haskell you would just use Eq , most of the time.) Welp, TIL that a partial equivalence relation is an equivalence relation that isn’t reflexive (!). The example in the docs for PartialEq is that NaN != NaN, so floating point types implement PartialEq but not Eq. 😬²
• Dave was using some types called Person and Pet for an example and kept saying things like “put the Pet in a Box” and “when the Person dies, the Pet dies, too” and it was all very sad.
• Recursive types have to be of finite size, so for example, for an Expr enum type for an AST, apparently you need to use Box when you refer to an Expr inside an Expr. For the record, this sucks and is ugly.
• It’s the end of day 2 of this 5-day course and I’m, uh, almost done with the lexer. :lolsob: Today I finally got the multi-character operators and string literals done. I still have to deal with numeric literals and keywords, and then I can finally move on. Also, my lexer is absolutely hideous and the error handling is laughably bad! Oh, well!

Day 3

• I finished my lexer and moved on to parsing today! I took some time to make my lexer nicer once I got it passing tests, and that brought me joy.
• The style Dave’s lexer is written in seems very different from mine. For instance, self doesn’t occur in my code at all. I think he hewed closely to the style of the Nystrom book, but I didn’t know how to do that in Rust, so – I didn’t.
• I got hung up on data structures today. I wanted a mapping from keywords to token types. This data structure will never change, so I wanted it to be static. Well, it turns out that you can’t have a static HashMap in Rust. After much flailing, I didn’t use a data structure at all and just wrote a function that pattern matches on strings and returns token types. The HashMap would’ve been overkill anyway – but I dunno what would’ve been idiomatic.
• We continued with the Pet and Person examples, and they got sillier and sillier. We kept saying things like, “Maybe the groomer should have borrowed your pet instead of taking ownership of your pet” or “When you get your dog back from the groomer is it the same dog or is it a different dog?”
• The first parsing-related project in the course was just coming up with an AST representation and then writing a pretty printer. That was easy, but parsing itself is going to kick my butt.
• I find the book’s example parsing code to be incredibly hard to follow. Dave doesn’t seem to be a big fan of it, either. His own example parsing code (in Python, for a tiny toy language) is more helpful to me, but I still think parsing is going to kick my butt. It is quite possible that parsing is as far as I manage to get this week. (Although, once I finally have an AST, I imagine that I can bang out an evaluator for at least a subset of the language really fast.)
• Sorry, but I’m going to get on my soapbox about the HashMap thing some more. Is there not a nice simple lightweight association list data structure in the standard library? I couldn’t find one. I would be happy to just call lookup on a vector of tuples, but do I have to write it myself? Surely it’s already there and I missed it, right? Like, come on. I really, really do not want or need “resistance against HashDoS attacks” for my *checks notes* toy interpreter’s token lookup table.
• Even if I don’t make it past parsing, this course is serving the purpose that I hoped it would, which is to get me writing Rust in a semi-serious way (again). Rust is nice. I know everyone says this, but I have to say it too: the user experience is nice – and I’m not even using any of the fancy-pants tooling that exists these days! I just mean simple stuff, like error messages are thoughtful, and it’s easy to write and run tests, and docs search works. So much love and care was put in. ❤️

Day 4

• I talked with some people on Mastodon last night and I realized that maybe I could write a macro that solves the HashMap problem I was complaining about yesterday. I didn’t get a chance to attempt it, though, because…
• I spent the whole day on parsing. I had a complete mess that didn’t really work. Then, after a conversation with Dave late in the day, I overhauled it, and now it’s pretty and works!
• I’ve never actually written a parser from scratch before (except in Scheme, for Scheme, for my Scheme compiler course in grad school, and that totally doesn’t count), and I didn’t expect to actually like the code at the end. It’s really kind of magical.
• We talked a bunch about lifetimes and borrowing and stuff in class today, but I was honestly pretty distracted with the parsing stuff and wasn’t paying close attention.
• It will be a piece of cake to write a simple expression evaluator now. I’m not that worried about variables – I’ve written a lot of environment-passing interpreters – but I am worried about how to deal with variable mutation. I don’t know how I’m going to handle that, and I might run out of time for it, since there’s only one day left. That’s kind of too bad, because that’s the part of the project that would force me to confront interesting corners of Rust. Well, we’ll see.
• My parser, like my lexer, is in a very functional style. self still doesn’t occur anywhere in my code. Dave was like “sooner or later you’re gonna have to go over to the dark side”, but, empirically, no, I don’t. (It’s not actually that I’m opposed to writing things in a more object-oriented style! It’s that I literally do not even know how to do it in Rust. I guess I could look at Dave’s Rust code more. I haven’t been doing that.)
• There seems to have been a lot of attrition in the course. For a big chunk of today, it was only Dave, one other person, and me. Apparently someone dropped the course because it was moving too slow for them. (That has, uh, not been my experience.) Other people had to bail because life happened.
• I wonder if maybe I should have taken this other course, which is the one Dave suggested to Shriram. I think it would’ve been easier for me. Oh, well – challenge is good!

Day 5

• The course is officially over. I learned a ton! I didn’t get that far on the actual interpreter (lexing and parsing alone took four days, and then today I banged out a simple evaluator for a small subset of the whole language, but even that involved some interesting design choices and some stuff I hadn’t thought about before). I definitely got a lot better at Rust, which was the goal.
• I developed some strong opinions about the Nystrom book. Pedagogically, I don’t much care for it as an introduction to language design and implementation. As one example: Chapter 5 is supposed to be about ASTs. Java is so ill-suited for the task that the book instead does this metaprogramming thing to generate the AST code, which is a neat hack, but it’s completely beside the point of what an AST is all about! I would be very confused if it were my first exposure to the concept.
• Also! Modern Java has enums and pattern matching and stuff! It wouldn’t have to be done in this boilerplatey, verbose way that necessitates a bunch of automation just to *checks notes* define an AST type! But that’s how the book does it.³
• Another complaint about the book is that there’s so much ink spilled about operator precedence. Really? For Fisher-Price: My First Interpreter? Words can scarcely describe how little I care about operator precedence.
• Anyway, enough complaining. On my first quick 20-minute hack-up of the expression evaluator, I made a beginner mistake: I evaluated subexpressions and then tried to do Rust operations on them, but of course I couldn’t because they’re Lox values, not Rust values. But this raised a design question: implement a bunch of traits (like Neg, Not, Add, Sub, etc.) for Lox values, or convert Lox values to Rust values so you can do normal Rust operations on them? I went with the latter.
• I ended up having to think about some design choices more than I expected! For instance, I decided that it should be okay to use comparison operations on arguments of different types, but that the result should always be false. So, 3 <= "hello" evaluates to false, and 3 > "hello" does as well. I could imagine how this behavior might be surprising. There’s a lot of nuance here. (There might be a “correct” semantics for Lox, but I didn’t bother to read the book in detail to find out.)
• Part of the point of this course was supposed to be that dealing with things like mutable variables in Lox would force people to confront thorny issues with ownership in Rust. I didn’t get that far, but Dave said that in the multiple times he’s taught this course, everyone has implemented the environment incorrectly by using cloning where they shouldn’t – but they never notice the problem, apparently because it doesn’t surface until you get further in the book than this course goes!
• We spent a lot of time talking about ownership and borrowing. One interesting question is: how to express co-ownership of an object? Returning again to the “pet” example, we talked about how you could model a situation where two people co-own a pet and should both be able to feed the pet (which mutates the pet!). This made talking about the example even sillier, of course. We kept saying things like, “Instead of a person having a pet, they can have a ref-counted pet.”
• Had I gotten further on the interpreter, the ref-counting thing would have been relevant for correctly managing the environment in Lox. But I didn’t even get as far as implementing mutable variables, since, again, lexing and parsing took 80% of the time. I probably would’ve gotten through those parts faster if were either more familiar with Rust, or if I had ever in my life implemented a proper lexer or parser before! I’m still happy with how much I got done, though.
• I thought it was kind of a bummer how many people seemed to disappear from the course. One person apparently said the course was going too slow for them, which makes no sense to me. The project was very self-directed, and every aspect of it had fractal complexity. You could spend the week just thinking about how to make error reporting good. (Dave kind of did this.) Or you could spend the week just trying to figure out how to allocate the barest minimum of memory. (Dave did a little of this.)
• All in all, I’m really glad I did this! I didn’t get that far on the actual interpreter, but it runs and does stuff, and I implemented a few things I had never implemented before. I don’t think I had any new insights about interpretation as such, but that wasn’t what I was going for. I did get better at Rust, which was what I was going for.
• Dave invited us to sit in on the “Ruckus” course for free, so I hope to do that at some point, if I can make the time!
• Last thing: I now have a Rust thing I want to build! I want immutable association lists that are constructed at compile time, so you can use them in a static initializer. Basically, I think what I want is something with the interface of the alist crate, but instead of being backed by a Vec, it would just be backed by, I guess, a plain ol’ array of pairs. So, static, like the phf crate, but without all the complexity of phf.
• Okay, actually, that wasn’t the last thing. There’s something else: programming is cool and fun! I don’t write a lot of code in my day-to-day life, and it was really nice to spend a whole week doing almost nothing but that. tokei says I wrote 1262 lines of Rust this week (a huge fraction of which is tests), not counting my initial attempt at a parser, which was a non-working mess and got thrown away. It was extremely satisfying to make something come to life completely from scratch.
• Also: my laptop is getting a bit long in the tooth, and I grow weary of macOS. I had been thinking about getting one of those pretty purple Framework laptops, putting Arch or something on it, and using that for the course this week. I was stoked! And then the Framework fiasco happened, I no longer wanted to give them business, and I was bummed about my personal computing situation and by extension, less excited about the course. But it ended up being fine! The Rust tooling all worked great! ❤️

Some final thoughts

I’m very happy to have now had the experience of (a) finally having written a lexer and parser from scratch, and (b) having done it in Rust specifically. But I agree with Shriram that this wouldn’t have been a good way to learn about “the essence of interpretation”! Fortunately, learning about “the essence of interpretation” wasn’t my goal – I already feel pretty comfortable with that topic.

Slava Pestov asked what language implementation book I do like, if not the Nystrom book. I don’t really know if I have a favorite – I learned about language implementation first by taking classes from Dan Friedman and Kent Dybvig at Indiana University (and those courses didn’t use books), and then by working on the Rust compiler as an intern. I don’t use a book in the PL course I teach now, either. That said, Jeremy Siek’s compilers book (in Racket and Python) attempts to distill the Indiana approach – which was particularly formative for me – into a book. So maybe that book is my favorite. (In fact, the Racket edition is the only book that I’ve ever written a back-cover blurb for.)

Conflict-free replicated data types – CRDTs to their friends – are data structures designed for fault tolerance and high availability in distributed systems. They replicate the same data across many physical locations, which helps ensure that some replica will be available and close at hand when clients need it. CRDTs have traditionally been taxonomized into state-based and op-based flavors. State-based CRDTs synchronize with each other by periodically sending their local state to each other, while op-based CRDTS synchronize by sending a stream of locally applied operations. It has long been known that these two flavors of CRDT can “emulate” each other: if you have a state-based CRDT, you can turn it into an op-based one by putting a kind of op-based wrapper around it, and vice versa. Shapiro et al. described these “wrapper” algorithms in their famous 2011 article introducing CRDTs.

But…what does “emulate” actually mean? In what sense does an emulated CRDT object actually behave like the original? We argue that this question actually matters, because researchers love to publish results about one or the other of state-based or op-based CRDTs and then argue that their results are general due to the existence of Shapiro et al.’s wrapper algorithms. For instance, in “Automated Parameterized Verification of CRDTs”, Nagar and Jagannathan write that their technique for op-based CRDTs “naturally extends to state-based CRDTs since they can be emulated by an op-based model”, and in “Katara: synthesizing CRDTs with verified lifting”, Laddad et al. write that their synthesized state-based CRDTs “can always be translated to op-based CRDTs if necessary”. But what results about an original object actually “transfer” over to an emulated object when we do this wrapping? That’s the question we tackled in this paper!

We specify and formalize CRDT emulation in terms of simulation by modeling CRDTs and their interactions with the network as transition systems. It turns out that emulation can be understood as weak simulations between the transition systems of the original and emulating CRDT systems. Getting the details right here was rather involved, because state-based and op-based CRDTs place different requirements on the behavior of the underlying network, both with regard to causal order of messages, and with regard to both the granularity of the messages themselves. With our main result in hand, though, we can then pretty straightforwardly get a good old-fashioned representation independence result about state-based and op-based CRDTs: client programs indeed can’t tell which flavor of CRDT they are interacting with, as long as they are limited to making certain (realistic) observations.

This paper has been in progress for more than two and a half years. Our collaboration got under way when Nathan and Stelios met way back at POPL 2023, when Nathan was presenting a different (but similar in spirit!) project at the POPL Student Research Competition. Nathan and Stelios got to talking, and we all began collaborating on what would eventually become this paper. Nathan presented some early ideas at CALCO in 2023, but the journey from there to this paper was long and challenging, and it’s wonderful to see our efforts finally bearing fruit!

It was Nathan’s idea to use different colors in the paper for the op-based and state-based CRDT semantics respectively, and to me, that suggests a tantalizing analogy to a long line of work on compiler correctness, like in Patterson and Ahmed’s “The Next 700 Compiler Correctness Theorems” (or lots of Amal’s other work). Of course, Amal would probably be doing this with logical relations instead. But it’s cool (and, I guess, not surprising in retrospect!) to see that emulator correctness is kind of like compiler correctness, and I’d like to continue to explore this direction of research beyond CRDTs in the future. Emulation is everywhere, and what it means for an emulator to be “correct” is an interesting question!

I’m pretty sure I met Alan at the first academic conference I ever attended, which was ICFP 2010, but he was a regular in that community for decades before that. Other people of course knew him far longer, and far better, than I did. Jeremy Gibbons’ lovely eulogy, which he gave at Alan’s Celebration of Life in November, highlights the incredible breadth and depth of Alan’s career and makes me wish I had another twenty years to talk shop with him. Robby Findler’s remembrance of Alan, which he shared at ICFP 2024 a few months after Alan passed away in July, also touched me deeply.

Robby and Jeremy represent a community for which Alan’s passing is a tremendous loss. But one thing that has really amazed me over the last year has been to see how many communities Alan was part of, and the incredible number and variety of lives he touched. When his health took a turn for the worse this spring, I exchanged emails and Signal messages about Alan with people who I know in completely different contexts – people who don’t know each other, but who had in common a connection to Alan, and who thought fondly of him. Academics; open source software folks; people considerably older or younger than me – he was part of all of their worlds.

While I was never fortunate enough to collaborate on research with Alan, a project we did do together was organizing captioning of all the ICFP 2020 and 2021 talks – the main thing we accomplished as accessibility co-chairs on the ICFP organizing committee in those years.¹ Captions make conference talks better for everyone. They improve accessibility for Deaf and hard of hearing people (as well as people with a mild degree of hearing loss), non-native speakers of the language being used (a large fraction of the ICFP community), and folks with auditory processing issues or ADHD. Last but not least, they provide a useful searchable text record of talk content. Automatic speech-to-text tools aren’t good enough – although an automated tool might produce something useful to get started with, the task requires expert human attention.²

ICFP 2020 was unusual in that authors pre-recorded their talks. We got videos from authors, assembled them into sessions, and sent those off to a professional captioning vendor. Unfortunately, we picked an inferior captioning vendor, so the captions we were able to get were often wrong. Alan then personally went through a large number of the talks and made corrections in places where the professional captioner got a piece of jargon wrong, lacked context for what was going on, or didn’t understand a speaker’s accent. I corrected some of the talks myself as well, but Alan did many more of them. You need only look at a few of Alan’s commits to witness his painstaking attention to detail and vast domain expertise at work.

After our correction pass, we also organized a process by which the speakers themselves could submit corrections to their captions, which caught further issues that Alan and I missed. (An amazing volunteer, Matt McCutchen, then handled the process of chopping up the session videos into individual talk videos and syncing the corrected captions with each of those individual videos.) I’m happy to say that in the end, the 2020 captions were high quality.

At ICFP 2021, which again had pre-recorded talks, we changed our process and asked authors to provide their own captions for the regular talks, and I’m happy to say that 97% of them actually did! For the plenary events, such as keynote talks and awards presentations, as well as for the PLMW workshop, we had high-quality live captioning thanks to White Coat Captioning, a fantastic captioning vendor. A large part of the reason we were able to afford this high-quality live captioning, by the way, was because Alan was also serving as the industrial relations chair for the conference and was able to line up financial sponsorships.

Alan had brain cancer, and last fall, as his health began to fail, he began having trouble understanding spoken language, although reading wasn’t a problem. This would of course be terrifying for most of us. But Alan had a typically laid-back attitude about it and he mentioned that he himself could now unexpectedly benefit from the work he’d done a few years earlier on captions.

(Am I politicizing Alan’s illness and death right now to argue for better accessibility affordances at conferences, more empathy for our colleagues who need them, and less dependence on unreliable AI tools? You’re goddamn fucking right I am.)

In general, whatever life threw at Alan, whether it was serious health issues (he also had MS) or ill-conceived corporate layoffs (he was part of the amazing Servo team that Mozilla gave the boot to in 2020), he somehow always handled it with serenity and found the positive side of every situation.³ He seemed to enjoy every day he was alive. He posted frequent smiling selfies and was happy to have outlived Henry Kissinger. Robby said that Alan had not only “syntactic serenity” – the shallow kind that has become a meme – but “semantic serenity, a deep sense of joy and acceptance of whatever it was that was there in front of him” – and I can’t think of a more fitting way to describe Alan.

In 2025 and beyond, may we all remember Alan fondly and try to live up to his example.

It’s finally done! 🎉 I am so excited to announce “Communicating Chorrectly with a Choreography”, the first zine from my research group. You can read it online, or print your own free copies to read offline!

Making research zines has been a dream of mine for a long time. Back in 2019, I experimented with zine creation as an optional assignment in my undergrad distributed systems class. In 2021, part of my NSF CAREER proposal involved integrating zine creation into my team’s research process. When that proposal was awarded in 2022, the next step was to recruit a student to work on zines with me, but it had to be the right person. The next time I taught undergrad distributed systems was in winter 2024, and I revived the zine assignment with the not-so-secret ulterior motive of finding a student who had the right combination of interests and skills.

Ali Ali’s course project blew me away, and I hurried to apply for REU supplement funding for him to do more. My REU supplement request was funded, and Ali and I began working together on the zine in July. “Communicating Chorrectly” is the result of a six-month collaboration. Ali is responsible for all of the drawings (though I made suggestions here and there), and we worked together on the writing.

Have I mentioned that Ali is amazing? He’s now graduated with his BS in CS from UC Santa Cruz and is on the job market – you should hire him! I can vouch for his strong performance in both my PL and distributed systems courses, but much more importantly, he’s a great collaborator: clever, creative, and a joy to work with. His work on the zine showed me that he deeply got the concepts and could craft a compelling story around them. Please hire him!

Now, about the zine itself! Our goal was to create an approachable and fun introduction to choreographic programming. It’s not specific to any particular programming language, but near the end we mention a few choreographic languages, with a particular focus on Choral and my group’s own work on HasChor, led by my awesome PhD student, Gan Shen. One fun thing is that working on the zine was apparently the push we needed to finally create a logo for HasChor, after a year of talking about wanting one. The logo concept was Gan’s idea, and it was beautifully realized by Ali!

It may not surprise you to learn that making just one zine took much longer than I expected – this was supposed to be a summer project – and the zine doesn’t cover nearly as much material as I originally thought it would. But I’m hoping that this zine will be the first of many, and starting in January I’m going to be on the lookout for my next student collaborator. It would be fun to do one about causal separation diagrams, as well as some other exciting work we’ve got in the pipeline!

I’m especially proud of the fact that, thanks to our NSF funding, I was able to pay my student collaborator a reasonable stipend for this labor-intensive project, and I intend to keep applying for REU supplements so that I can hopefully continue to do that. Research communication and outreach is crucially important. People need to get paid for their work. Undergrads need to get paid, but often don’t.

I’m also happy that we finished the zine just in time for me to hand it out to folks here in Edinburgh at the IFIP Working Group 2.11 meeting, which I’m attending as a guest this week. (Special thanks to Ohad Kammar for getting color copies printed for me!) And being here in Scotland among PL folk is of course also making me think fondly of Alan Jeffrey, who loved comics and was known to have made some of his own. I would have loved to be able to share this zine with him, among so many other things.

While getting ready to teach my grad distributed systems course this fall, I found myself once again flipping through Cheriton and Skeen’s rather scathing 1993 article “Understanding the limitations of causally and totally ordered communication”.¹ One of Cheriton and Skeen’s complaints about causally ordered communication is that it does not enforce the ordering constraints that they care about. They write:

[T]he correct behavior of an application requires ordering constraints over operations on its state, and these constraints are typically stronger than or distinct from the ordering constraints imposed by the happens-before relationship. Such ordering constraints, referred to as “semantic” ordering constraints, run the gamut from weak to strong, and they may or may not require grouping as well. Example constraints include causal memory [1], linearizability [12], and, of course, serializability. Even the weakest of these semantic ordering constraints, causal memory, can not be enforced through the use of causal multicast [1].

While it’s a good point that there are many important application-level ordering relationships that are not captured by the happens-before order, the last sentence above caught my attention because it seemed counterintuitive. Of course we can’t expect the causal order to give us linearizability or serializability. But causal memory is a distributed shared memory abstraction in which “reads respect the order of causally related writes”, and it certainly seems like it ought to be the kind of thing you can implement using good old causal-order-enforcing communication primitives. So, why can’t you? Let’s dig in!

The paper that Cheriton and Skeen cite as “[1]” there is “Implementing and programming causal distributed shared memory”, published in 1991 by Ahamad, Hutto, and John. The more often cited paper for “causal memory” is actually not this 1991 paper, but rather, “Causal memory: definitions, implementation, and programming”, a 1995 follow-up with some of the same authors. (Of course, Cheriton and Skeen didn’t cite the 1995 paper, because it did not exist yet when they wrote theirs.) Unfortunately, the 1991 paper is not open access; here’s a copy. In this 1991 paper, Ahamad et al. explain that while causal memory is indeed “closely related” to causal message ordering (which is a perennial topic around here), broadcasting writes and delivering them in causal order doesn’t quite get us causal memory. They write (emphasis mine):

As we have said, causal memory is closely related to the ISIS causal broadcast and, thereby, to the notion of causally ordered messages. But causal memory is more than a collection of “locations” updated by causal broadcasts. There are significant differences in the two models.

One way to relate the two models is to assume that each processor has a copy of the memory (a cache) and writes are sent as broadcast messages to all processors. When a message arrives at a processor, it updates its memory by storing the value contained in the message into the appropriate location. A read by the processor returns the value in its memory. It may seem that when the message delivery order preserves causality (for example by using the causal broadcast protocol of ISIS) the values returned by read operations will satisfy the requirements of causal memory. This, however, is not true.

They then give an example of an execution of this collection-of-locations-updated-by-causal-broadcast-based approach that would not be allowed by causal memory. For me, a Lamport diagram makes their example execution easier to understand, so here’s one, showing broadcasts for writes and the contents of each process’s cache:

Here, we have three processes, \(P_1\), \(P_2\), and \(P_3\), each of which has carried out a sequence of read and write operations. I’ve borrowed Ahamad et al.’s notation for these: A write operation \(w(x)v\) writes the value \(v\) to location \(x\), and a read operation \(r(x)v\) reads the value \(v\) from location \(x\). The boxes in dashed lines are each process’s local memory, and messages between processes are causal broadcasts, which happen on each write.

The part of this execution that violates causal memory is the read of \(x\) on \(P_3\): \(r(x)2\). From what I can tell, this wouldn’t happen under causal memory, for a subtle reason described earlier in the paper, in section 2:

However, an intervening read operation \(r(x)v'\) serves notice that \(v\) has been overwritten and is sufficient to eliminate \(v\) from \(\alpha(o)\) as well.

Here, “\(\alpha(o)\)” is what Ahamad et al. call the live set for a given read. Under causal memory, every read has to return a value from the live set for that read. Because there could be multiple writes that causally precede a read, in general there might be multiple values in the live set for a read, and under causal memory it’s fine to choose any of them.

In this particular execution, both the write \(w(x)5\) on \(P_1\) and the write \(w(x)2\) on \(P_2\) causally precede the read \(r(x)2\) on \(P_3\). So it seems as though \(5\) and \(2\) should both be in the live set for the read \(r(x)2\). But! There’s an intervening read on \(P_2\) that reads \(5\). That means that \(2\) is eliminated from the live set, and so under causal memory, the read of \(2\) on \(P_3\) would actually be wrong.

A perhaps more intuitive way to explain the issue is as follows: if a process reads a location, then the value it reads has to have come from a causally preceding write on some process. There will be at least one causal path from the write to the read. If there are multiple causal paths to the read from different, concurrent writes, then one of the written values will be read, and under causal memory, it could be either one. But if these multiple causal paths to the read also both pass through some causally preceding “intervening read”, and that intervening read “picks a winner”, then under causal memory, the later read has to pick the same winner!

Here’s the same Lamport diagram, but now with causal paths highlighted to attempt to illustrate the bug:

Here, a causal path starting at the write \(w(x)5\) is yellow, and a causal path starting at the write \(w(x)2\) is blue. Both paths are heading for the read of \(x\) on \(P_3\). The paths overlap for a while, as shown in green. But then, during that overlapping part, there’s the read \(r(x)5\) on \(P_2\). Since the “winner” is chosen to be 5 by that read, the causal path starting at \(w(x)2\) has been effectively “cut off”, and now the rest of the causal path can only be yellow. Therefore, under causal memory the read of \(x\) on \(P_3\) should have been 5, and so this is a buggy execution.

So, causal memory admits fewer executions than the set-of-locations-updated-by-causal-broadcasts approach. Although I had read the 1995 causal memory paper, I didn’t realize that this “intervening read operation” thing was a thing – it didn’t sink in for me until looking at this 1991 paper a couple days ago. It’s interesting how a read – not a write, just an innocent little read! – on one process can have an effect on what a different process is allowed to read. My student Jonathan Castello remarked that these so-called reads should really be thought of as just another flavor of write, since they’re effectful.

Perhaps it won’t come as a surprise, then, that in the implementation of causal memory that Ahamad et al. show later in the paper, reads do in fact involve inter-process communication! The implementation enforces the causal memory policy using cache invalidation. Every location has a designated owner process. If you try to read from a location you don’t own, and your cached copy of it is invalid, you have to check in with the owner. It’s not exactly the most “local-first” design, as the kids these days would say.

In exchange, unlike in the set-of-locations-updated-by-causal-broadcasts approach, you can be assured that \(P_3\) will not read \(2\) out of \(x\) if \(P_2\) already read \(5\) out of \(x\). Whether this tradeoff is worthwhile probably depends on what you’re trying to do!

If you’re not familiar with !!Con, it’s a radically eclectic, radically inclusive, radically affordable (pay-what-you-want!) independent nonprofit computing conference. I co-founded !!Con with a group of friends back in 2014, and there’ve been a bunch of iterations of it since then.

!!Con consists almost entirely of ten-minute lightning talks about “the joy, excitement, and surprise of computing”.  Any computing-related topic is fair game – as long as the title of the talk contains at least one exclamation point! Sumana Harihareswara’s “Toward a !!Con Aesthetic” beautifully captures a lot of what I think makes !!Con special.

This year is extra-special – it will be the last !!Con, and we’re doing something different: for COVID safety reasons (and just because we want to), we are holding the conference completely outdoors! It’ll be held in the courtyard of the Baskin School of Engineering, on the campus of UC Santa Cruz (where I work), in sunny and scenic Santa Cruz, California, USA. (UC Santa Cruz was also the site of the two previous west-coast editions of !!Con, !!Con West 2019 and !!Con West 2020, the latter of which was the last in-person !!Con before the pandemic became a pandemic – but those were indoor events.)

You might think of Santa Cruz as a touristy beach town, and you wouldn’t be wrong – but it’s also a secluded oasis of coastal California redwoods, about an hour’s drive from the bustle of Silicon Valley. It’s a wonderful place to spend a weekend!

Now, here’s why I’m asking for your help. Earlier this year, the !!Con 2024 organizing team decided to quit Twitter, where we had 5k+ followers, in favor of federated social media not owned by Elon Musk. We are now on Mastodon, where we have a small fraction of the following we once had.

We began selling tickets five days ago. In the past, !!Con tickets have often sold out in a matter of hours, or even minutes – truly, they’ve gone scarily fast at times. But this year, while our first 50 tickets went very quickly, presumably to our most hardcore fans, we’ve seen a slump after that. As of this moment, we’ve sold 99 tickets, when we were hoping to sell about twice that many.¹

While it’s possible that people just don’t care about !!Con this year, I suspect that a big part of the problem is that we’re failing to reach our usual audience, perhaps as a result of having left Twitter. A friend mentioned that, despite being on our mailing list, he didn’t realize that tickets were on sale until he happened to look at our website a couple of days ago. (We really don’t want to abuse our email list – we tell people when they sign up that we’ll only send them four or five emails a year – but the result is that our handful of emails get lost in a blizzard of marketing emails. My friend told me that in the few days since we sent our announcement about ticket sales opening up, he’s received eleven marketing emails from Petco.)

My worry about slow ticket sales is exacerbated by the fact that, due (I guess) to the ongoing tech downturn, we weren’t able to line up any corporate sponsors this year. (Know anyone who still wants to sponsor us? Send ‘em here!) That’s also the reason why this year, our tickets have a suggested price of $256, which is higher than it’s been in the past. Although $256 is only a suggested price, we do have to sell a certain number of tickets at a certain price to break even. And break even is all we’re trying to do – we’re a nonprofit organization, and this is the last !!Con, so we intend to leave the bank account more or less empty. But we still need to be able to pay our bills, which are high this year due to our outdoor venue. We’re having to rent a bunch of stuff: a portable stage, chairs, tents, and a pricey outdoor “video wall” because projection doesn’t work very well in bright daylight outside.

So: we really need your help spreading the word about !!Con so we can sell our tickets, pay our bills, and have a successful last event! If you’re reading this and you want to help, here’s what you can do:

• Most importantly, please spread the word about !!Con to anyone you know who might want to go!
• If you live in the area or it’s not too far for you to to travel, you should join us in person for !!Con if you can! Get your tickets here!
• If coming in person is not an option, we have an online-only ticket for a suggested donation of $8! This’ll get you access to our 2024 Discord; Discord was a popular feature of the online-only !!Cons in 2022, 2021, and 2020, so we’re keeping it this year.

Thank you for helping us out!

I co-founded !!Con with a group of friends back in 2014, and the team went on to organize another !!Con conference each year for several years. Helping run these first several !!Cons was an absolute highlight of my life. If I hadn’t gotten an academic job in 2018, my secret plan was to quit my corporate job anyway and throw myself full-time into !!Con fundraising and organizing. There was incredible demand for what we were doing, and my hope was to scale !!Con to lots of conferences in lots of places.

I didn’t end up doing that, because I did get an academic job in 2018, which has been all-consuming. But I managed to make organizing !!Con part of my job by organizing !!Con West at UC Santa Cruz in 2019 and (early) 2020. These were both incredibly special events. They were undeniably !!Cons, in keeping with the !!Con aesthetic, but they made a point of “enthusiastically embracing the physical and social geography” of their west-coast venue.

Then COVID became a pandemic. The second and final !!Con West happened over the weekend of February 29 and March 1, 2020. We were, of course, aware of COVID, and we discouraged handshaking and put lots of hand sanitizer around the venue. But we didn’t think about masks or air filtration – few people were thinking about those things yet – and we had 200 people packed into very close quarters. In retrospect, that’s horrifying, and we were very lucky that the conference did not, so far as we know, turn into a superspreader event.

!!Con 2020, which had been scheduled to be held in person in May, switched to a remote format, and !!Con 2021 and 2022 followed suit. !!Con West did not continue beyond March 2020, which I justified by saying that a big part of the point of !!Con West was that it was in a particular physical place (it’s right in the name, after all!), so it wouldn’t be appropriate to have it as an online event. While I do think that’s defensible, the real reason I didn’t continue to organize !!Con West was because I was trying to navigate life as a tenure-track junior faculty member with a small child amid a deadly global pandemic during which I had no full-time child care for over a year, against the backdrop of a government that seemed eager to deport my students and take away my reproductive freedoms. Other members of the !!Con team were navigating similarly difficult circumstances. Perhaps it goes without saying that after !!Con 2022, the team was burned out and needed to take a year off in 2023.

I am not the same person I was when we started !!Con ten years ago. We were in our twenties and thirties then, and we’re in our thirties and forties now. Some of us got married; some of us started our own new ventures; some of us had kids; some of us took on more responsibility at work; and some of us did several of those things! It’s reasonable that a group of people’s priorities will change over time. And, of course, COVID greatly accelerated that reprioritization. So to me it’s not at all surprising that we decided that !!Con should come to an end.

But we didn’t want to fizzle out; we wanted to end with a bang, as it were. So a group of us decided that we would organize one last !!Con – here in Santa Cruz, on the site of the last !!Con that was in person (namely, !!Con West 2020), but with a COVID-conscious twist: we’re holding the whole event outdoors! (Also, we’re holding it in August rather than in February, which makes it easier to hold the whole event outdoors.)

Preparations are well underway: we’re currently reviewing 173 talk proposals, with the difficult task of narrowing it down to 30 or so; we’ve got two great keynote speakers on the docket; and we’re actively soliciting sponsors. (It turns out it’s really expensive to do A/V at an outdoor event. Can your organization help sponsor us so that we can continue our decade-long tradition of pay-what-you-want tickets? Get in touch!)

Our opening keynote speaker will be Dawn Walker, a researcher and designer who works to create lasting alternatives to existing ways of building technology. She has started a tech worker co-op, participated in community-led archiving of environmental and climate data, and schemed about mesh networking (to name just a few things). Since 2017 she has co-organized Our Networks, a conference about the past, present, and future of building our own network infrastructures.

Our closing keynote speaker will be Bruce Waggoner, Mission Assurance Manager at the Jet Propulsion Lab/Caltech, where he has worked for 39 (!) years supporting dozens of Earth-orbiting and deep space missions, and where he is part of the leadership team supporting the Voyager mission. Voyager 1 is the human-made object most distant from Earth, and Bruce’s talk at !!Con will tell the story of how the Voyager 1 flight team created a plan to patch its flight software – from over 15 billion miles away.

I love the juxtaposition of these two keynote talks. Dawn’s work draws on practices of local-first computing, while the Voyager mission is…as non-local as it is possible for computing to be. That’s what I wrote on Mastodon last month, but I’ll go even further: Dawn’s work embraces a DIY, grassroots, folk-computing aesthetic, while Voyager is a project that perhaps only a big, powerful nation-state could undertake. Yet, we can perceive a common thread: an emphasis on longevity, sustainability, and doing our best with the resources we’ve got. What a beautiful message to conclude !!Con with.

I don’t think that the end of !!Con is the end of the !!Con spirit. A new group of people will step up and organize a new event for a new era. Maybe it will be you! (But you should probably name your event something else! It was never easy to find us with a web search to begin with, and that was before BTS took our brand.)