Writing a pretty good paper in sixteen years if you're me

25 Nov 2024

One of my sidequests, the Dusa programming language recently reached a big milestone — a paper describing the language it implements will be presented at the Principles of Programming Languages conference in Denver this January. Despite having effectively left academic research as a career after I got my Ph.D. in 2012, and having effectively left academia about eight years ago, this is probably the top venue I’ve published in. I think it’s the best paper I’ve contributed to as well; I’m honestly not sure I can do much better work than this.

The sidequest started at the beginning of this year, or just over a year ago, or just under a decade ago, or sixteen years ago, depending on how you count. That’s something I wanted to think muse ramble rant write about, so here goes.

Ooh, logic programming! (2007-2008)

The very beginning was my first successful graduate school project all the way back in 2008, Linear Logical Algorithms. That paper was about using linear logic to allow a logic program to give more than one answer — in the language of the POPL paper, about using linear logic to describe some possibility spaces — in such a way that your logic programs would run in a predictable and fast way. So you weren’t just writing specs in logic, you were, in a meaningful sense, implementing algorithms.

This work never went anywhere, and I think there’s two reasons for that: one, it wasn’t quite general enough of a solution that you wanted to use it for lots and lots of problems, and two, I didn’t implement the ideas. Maybe an implementation would have led to more compelling examples, but I kind of doubt it. It was a good, limited idea, and it introduced me to the idea of cost semantics for logic programs, which is the idea that you should be able to reasonably predict the behavior of a logic program without actually understanding everything about how that program is implemented.

Puzzling over Answer Set Programming (2015-2023)

My spouse, Chris Martens, was in same Ph.D. program as me, and their Ph.D. was about using linear logic as a logic programming language to describe possibility spaces.

After Chris graduated, they started a postdoc working with some folks at UC Santa Cruz, who used something called Answer Set Programming (ASP) to describe possibility spaces. Chris and I both like linear logic in much the same way normal people like sports teams, so they would occasionally grump about it. But there was something that we found pretty strange going on: ASP was clearly pretty good at being a general solution that people wanted to use for lots and lots of problems, but as Chris explained to me a bunch of times, it seemed unnecessarily hard to actually explain what a program meant. And I agreed, because whenever Chris tried to explain what ASP was actually doing and why it worked I got frustrated. But I was busy and had a lot of stuff going on!

Creating Dusa (Fall 2023)

I started Recurse Center after leaving my job in October of last year, and immediately, badly, and unrelatedly screwed up my knee. This changed my plans for Recurse Center pretty radically, because I wasn’t able to be in New York in person very much. Recurse Center does a lot to facilitate remote participation, but there are certain types of collaboration that I’d hoped to do that are just, for me, hard when I’m not present in person.

But I did have a set of ideas I could think about independently and with Chris that had been, at this point, simmering for years, and I turned those into a language implementation. It was kind of sort of related to ASP, and an ASP is a viper, and there’s a type of viper called Dinnik’s Viper, and so at first I named the repository Dinnik, but then the American Ornithological Society decided to not name birds after dead white guys, and I thought that made sense, so I named it Dusa to keep broadly on the snake theme.

And it kind of worked, and let Chris and I do some answer-set-programming like things in a way that made some sense to me, and seemed to also make a fair amount of sense to Chris as well. I was able to write up a definition of how the language was supposed to work that fit on a page, and we were both pretty happy with that.

Advent of Dusa (December 2023)

In December my knee was in good enough shape that I could spend some time at Recurse Center in Brooklyn, and lots of people there were doing Advent of Code, a yearly programming event of 50 programming puzzles over 25 days that I’d poked at in the past but never completed.

Given that I’d just built a programming language, I decided to try and do Advent of Code using my new language, and write up what went wrong, and thus was born the Advent of Dusa. There was a little bit of that energy in the air; Nicole Tietz-Sokolsaya was also at Recurse Center and did some AoC in her language, Hurl.

What surprised me was that this kinda worked. I was able to solve the vast majority of the AoC problems with Dusa with a minimal JavaScript wrapper. And I found myself able to do stuff that would be more annoying to do if I was using a different programming language. This was actually a huge turning point, because it convinced me that this was possibly a general solution that people might want to use it for lots and lots of problems — exactly what the linear logical algorithms language was not.

What did we just do? (Most of 2024)

The one page definition of Dusa was nice, but it wasn’t that nice. Chris and I agreed on that, but we didn’t quite have the words to explain what that meant, except to say that we felt like we needed a denotational semantics for Dusa. (I don’t recommend that Wikipedia page as an explanation of anything, for what it’s worth.) When Chris attended POPL 2024 in London, they reconnected with a mutual graduate school friend, Michael Arntzenius, who had actually done work with the semantics of logic programming, and who was interested in helping us.

We spent a fair amount of time in January and February preparing a paper that we submitted to ICFP 2024 which presented that one-page description of the language that Dusa implements, which we named Finite-Choice Logic Programming. It also included a denotational semantics that Chris and Michael developed, a discussion of the algorithm I’d implemented in Dusa, and some details about a predictable cost semantics for the language, connecting all the way back to that work I’d done in 2008. Unfortunately, we weren’t able to prove that any of those three things (the one-page description, the denotational semantics, and the algorithm) were the same, though we were pretty sure they were the same, and that was a pretty reasonable justification for ICFP not accepting the paper.

All three of us did a bunch more work to actually write proofs that all these things agreed with each other, and to explain everything better to avoid some points where our ICFP submission had been confusing to readers. We submitted that to POPL, and I was very pleased (and also relieved) when it was accepted.

Is that actually what I did? (October-November 2024)

Something that’s been very time-consuming but extremely rewarding has been, in the last month or so, taking all the lessons we learned about Dusa by writing a paper about that, and rewriting Dusa. It turns out that a lot of the math that we needed to give finite-choice logic programming a denotational semantics was already there in my implementation, but I wasn’t thinking about it as “code implementing some mathematical ideas,” I was thinking about it as “a hack that I don’t really understand that makes the program stop running forever in this situation that I don’t quite understand.”

My former Ph.D. advisor Frank Pfenning has talked about this cycle before: I believe that contextual modal type theory in particular was a logic that explained, after the fact, a couple of things about the Twelf implementation that were originally put there as weird hacks. This was my first time experiencing it, though! And actually updating the implementation to explain those hacks in terms of the mathematics that we’d developed over the past year was just great.

So here’s a software engineering process that only works if you’re me, have already thought about the problem for 10 years, and also married someone with excellent taste in programming languages who will share your excitement about ideas and also find other collaborators that can help you out and also will put up with you spending months building stuff that doesn’t bring an income:

Diagram showing a cycle between 'Hack on system (1 month)', 'Hack with system (1 month)', 'Write paper (10 months')

Taking 5-10 times as long to understand and explain what you’ve done than it took to do the thing feels about right, honestly.

And it’s just in time for Advent of Code! I am, in fact, going to try to do an Advent of Dusa again this year, but given that I’m not actually a full-time Recurse Center participant, I’m not certain how successful I’ll be.

Beyond that, there’s a lot of stuff about the actual implementation and cost semantics that got mostly or entirely cut from the POPL paper to make way for the fact that we were able to actually prove things about the denotational semantics, and so I probably could ride this loop at least one more time if I get the opportunity and energy to do so. The parts that got cut were also more parts I’d worked on than parts Chris and/or Michael worked on, and because I have less career motivation than either of them to publish academic papers at the moment, I should really try to get some of those ideas out as blog posts rather than doing all the up-front work of writing big ol’ papers.

What have we learned?

So, I’m really pleased by how this all turned out, in trying to finish this blog post I’m also realizing I have some conflicted feelings about how many things specifically had to go specifically, unusually, (unfairly?) well in order for me to be able to participate in this cool research project in the way I have. I’ve now rewritten this section too many times for the short and informal note that I wanted this to be, so I’m going to leave this idea hanging for now, and maybe if I figure out what I want to say here I’ll follow up here or on Mastodon.

In the meantime, you can: