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.

Building the Agda MCP: field notes

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 MCP server I 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 became a pivotal design record. Four of the rules the server now runs on are in it, and each exists to address a defect I can name. The project page has the artifacts and the current numbers.