Skip to content

2026

The typechecker as a reward signal

A proof assistant answers one question all day long: is this term a proof of that goal? The answer is an exit code from a process that never reads your explanation of what you were trying to do. I have spent several months building a search loop whose every judgment comes from that exit code, so this is a report on the signal itself: what it is exactly, what it gives a loop that trains or evaluates a reasoning system, and the four things the measurements say it does not give.

The agent that never called the server

In July a Claude Code session working in ualib/agda-algebras formalized about 1200 lines of literate Agda, ran fifteen or so typecheck iterations and four full-library builds, and never once called the Agda server I had built for exactly that job. The server was configured. Its four tools were listed in front of the model on every turn. The session used agda from a shell prompt instead, every single time.

The session wrote its own post-mortem, and that document turned out to be the design record. Four of the rules the server now runs on are in it, and each one is a defect I could name rather than a principle I liked. The project page has the artifacts and the current numbers.

The quotient map is the identity function

Universal algebra is about quotients. Kernels, the isomorphism theorems, subdirect representation, the Birkhoff HSP theorem, etc. Every one of these takes the quotient of an algebra by a congruence. So a formalization of the subject, in a language with no quotient types, has to answer what 𝑨 ╱ θ means.

agda-algebras answers this question, twice. Each of two trees in that repository provides its own answer, and a comparison of the two is the most useful thing I could hand another practitioner, because it is concretely exhibited, rather than abstractly argued.