How I Came to Love Agda

vicāraḥ paramaṃ jñānaṃ
Inquiry is the highest knowledge.
 — Yoga Vasiṣṭha

I always wondered what it would feel like to live through the Industrial Revolution. Now I have some sense of how it goes, as I’ve been deep in contemplation and exploration about how to relate and adapt to the advent of the LLM.

It’s complex. Like a 19th century combine harvester or automatic loom, these are powerful and efficient, but also profoundly frustrating and more than a little dangerous. I observed that, like humans, the clearer you are with it, the more likely it is to provide you with quality work. Unlike humans, perhaps, the way to alignment is with logical precision.

This is how I found my way to Agda, a language that mathematicians use to help with formally proving math using Dependent Type Theory. I found that if I could prove something in Agda, and then show it to the LLM, I got both better context and output. It was a way of developing trust.

Agda’s language is fussy and arcane, and I fell in love with it. It has ways to allow it to be loose, leaving postulates (”let’s assume this is true”) and holes (”and then something happens here”), and ways to lock it down into a strict mode that allows none of that (”show me the receipts”).

I took up the challenge of trying to work in “strict mode” — no shortcuts, which reminded me of the strictness of 18th century counterpoint. And in doing so, I developed a way to build constructive proofs. The main function employed in this is what Agda defines as `refl` — Reflexive. It means that the two things being compared are exactly the same. Not a little identical — exactly identical, validated by machine logic. `refl` says only one thing: yes.

Here’s a very simple example of an Agda program:

If the program compiles, this is true (unless math is not real or there’s a bug in Agda). This is as close to true as I’ve been able to get, computationally. A point of truth that I as a human and the LLM as a software system can agree on, a contract that cannot wobble.

I love this method because it doesn’t involve argument in any way. No rhetorical tricks, no my-word-versus-yours. This is more in line with how musicians work together than with what I’ve seen in the business world. When an orchestra tunes, they all tune to the truth of the A440. When one locks into a pitch, one feels the truth of one’s alignment.

Agda has served as a bedrock for much of my programming and research in the past few months — if I can back up my software design with Agda, I can validate the correctness of my architecture and use it as a reference to validate the correctness of my code. The two formal systems buttress each other. As I’ve gotten into more abstruse systems, such as Category Theory, Topology, or Music Theory, this has come in very handy.

The net effect is that my LLM usage has become safer and more playful, thanks to the rigorous core. The tuning allows for more expression and less dissonance. It keeps me honest, tempers the LLM’s bombast, and grounds the whole experience.

My work with Agda has helped me deepen my understanding of the word “true” and what it points to. True is something one can feel, in the way that a bicycle wheel that spins smoothly is true — it does not wobble. This process is, in fact, called “trueing.” Truth is something one can hear, like a major chord in tune. Truth is answering the question “is this so?” with “yes, this is so.”