Skip to content

Tooling

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.