See Act I for an explanation of journaling RPGs.

I wanted to play a journaling RPG but didn’t have a deck of cards with me. Should I ask Claude for help?

It had certainly already occurred to me that I could get an LLM to just make up a cool custom-themed journaling RPG for me. But I didn’t really want to do that. I wanted to have an experience that was created for me by another human. Now though, it was occurring to me that I could have Claude write a simple program that simulated tracking the state of the cards as they would be arranged and manipulated on the table. Then I would still be playing the game that was created for me by another human, just aided by the tool that is the LLM.

It further occurred to me that I could wrap in another one of my current interests, which is Lean, the programming language. Lean was designed for formal verification and is used mostly, at least as of the time of this writing, for proving theorems in mathematics. But it is a fully-fledged programming language, and it can do anything any other programming language can do. In theory you could build a phone game or the next social media platform in Lean.

I am currently extremely enthusiastic about learning Lean, except that I haven’t really done that much of it yet. The reader might see parallels between this and my relationship history with journaling RPGs. But I thought if I can have Claude write this game simulator for me in Lean, then I can use that tiny, self-contained codebase as an object of study for better learning Lean. And also, for finally playing a journaling RPG.

After a few backs-and-forths with Claude, he produced a minimal spec. I then spent several hours reading through and trying to understand each line.

And this worked! I got a bunch more experience reading and understanding Lean syntax for a project where I knew exactly what it should do and where I was motivated to make sure it worked correctly. I learned about lots of little quirks of Lean, like the fact that subtracting natural numbers truncates at zero, or that the set of numbers from 0 to 5 is its own type, Fin 6. (The 6 isn’t special; every such finite set is its own type.)

But more than that I got a little bit more of an understanding of what formal verification looks like. I had asked Claude not just to implement the game but first to write out a behavioral spec for the game’s rules. This is a necessary stage of formal verification and there are parts of it that can feel counterintuitive on first exposure. The specs can sometimes feel like a copy of the implementation, especially with the simple examples one must pass through while learning.

A common class of thing one proves in formal verification is called an invariant, which is some property that holds on every step. For Borealis, the game I chose from the first act, an invariant would be that no card appears in the deck twice, or that the pawn is always on a face-up card. If you prove these properties for the initial deal, and then prove that every legal game action preserves these properties, then by induction you’ve proved that they will always hold true during the session.

After I read through the whole spec and was satisfied that I understood everything, I asked Claude to actually implement the game. This request was, as often seems to happen, over-eagerly responded to, and Claude pumped out another thousand lines of Lean code. Having worked my brain pretty hard to read the first several hundred lines and it being close to midnight, I just let out a big sigh, closed my computer, and went to bed.

The next morning I got up and asked Claude to redo the implementation work, without the features I didn’t ask for, and keeping the Git commit history more fine-grained.

After that came the play testing. I was pretty sure Claude got all the game behavior right on the first try so I wasn’t really testing the Lean implementation. Instead I was back in the mindset of being excited to finally try a journaling RPG and see how I liked it. The structured procrastination had done its job beautifully, and it was time to get down to the real work: playing.

It went so well that my journaling of the session came out as a basically fully coherent story. This has… never happened to me before? To be clear it’s not a story that I love. It does not, for example, treat themes of rationality, cultural heritage, or anything else that I would deliberately write a story about. But I like it, and the fact that it came out so easily on the first try was a pretty strong effect size.

In fact, I liked it enough that my play session journal is the third post of this series.

Act III coming soon.