In Praise of LACI

This is a short blog post about Prabakhar Ragde’s “Logic and Computation Intertwined”, or “LACI”, currently available online at

https://cs.uwaterloo.ca/~plragde/flaneries/LACI/

Here is a bad thing about LACI: every time I search for it, my search engine steers me toward articles about the tragic life of Laci Peterson.

Here is a good thing about LACI: everything else!

Specifically, LACI walks you through the process of building a small higher-order-logic theorem prover, using the same dependent typing bones as systems like Lean, and Agda, and Coq.

I have just finished using LACI as the first five weeks of a master’s-level course at Cal Poly, and I found it fantastic. Specifically, it has the part I most like about the definitional interpreter experience: you hear about a technical thing, and you think “yes, that sort of makes sense to me,” and then you try using or extending it and you realize “wow I didn’t understand that at all”, and then you figure out a fantastic new thing and you carry it around like a shiny stone for the rest of your life.

In fact, there are a number of shiny stones involved in LACI. Here are some of the ones that I appreciated the most.

First, intuitionistic proof theory (and maybe more specifically the BHK interpretation) comes up with a really fascinating way of talking about negation as an implication of bottom. Figuring out the propositional puzzles here, and how to prove certain things, is an absolute ton of fun (for a particular definition of fun, I grant you).

Second, dependent type theory pushes through a really mind-bending overlap between types and propositions: propositions are types. This leads to a really complete collapse between the boundary of terms and types. A quote from Moon over Morocco, presented in the show as a moroccan proverb and who knows maybe it is: “A devil takes one and makes two; a saint takes two and makes one.” In this case, collapsing the boundary between terms and types makes for some incredible richness, mixing lambda terms and forall terms (and many other things) in a mind-bending way.

For both of these, Ragde also provides a selection of excellent exercises. Formulating exercises in a domain like this is extraordinarily difficult; there are not a large pool of equivalent-difficulty problems that can be generated mechanically. A programming languages course has this same problem, if (like PLAI 2nd edition, for instance) the goal is to get you to implement an interpreter for some lambda-calculus-like language. Ragde does a very nice job of implementing core things, and then challenging you to implement satellite things that are hopefully just a bit out of reach, but not so far out of reach that things get hopelessly tangled. I’m in the final stages of coaching my students through an implementation of the natural numbers in Proust, and the problem is enlightening without being utterly soul-crushing.

I would also be remiss if I did not heap praise on the many side-notes and references that Ragde provides; many of the sections initiate potentially lifelong explorations of math and logic, and provide names and ideas for further investigation. This is the kind of thing that students sometimes complain about, but that curious thinkers delight in.

Another quote, this one from Ralph Sockman: “The larger the island of knowledge, the longer the shoreline of wonder.”

That link again:

https://cs.uwaterloo.ca/~plragde/flaneries/LACI/

Enjoy!