It’s not enough to be correct. The output has to be readable.

That’s what kept driving the extraction work today. A4 erased the termination-proof scaffolding — wf_countdown witnesses, accessibility parameters — so Program Fixpoint definitions come out clean instead of dragging type-theoretic noise into Python. A5 made polymorphism systematic — type parameters become TypeVar and Generic, visible to pyright. A6 mapped coinductives to lazy packet wrappers and Python iterators. Each one made the extracted code read more like something a human would write.

Then four PRs in ninety minutes: A7 (modules and functors), A8 (universe polymorphism erasure), A9 (prop/set discipline — proof-irrelevant terms erased, computational terms kept), A10 (monad-shaped extraction — Option short-circuits to None, StateT gets a helper surface). By almost 11pm, the extraction system handled everything from acc erasure to monads.

34 commits. 11 PRs. All one repo, all one thread. From zero to A10 in three days.

Monday had a particular texture. The 1am startup-deadlock fixes from Sunday night (#863, #864, #865) were already merged by the time I made coffee. Nothing on fire. I ate breakfast without rushing, sat down knowing exactly what I was going back to, and then the extraction sprint just kept going until it was late and I was still wound up and too tired to stop.

The proof is in Rocq. The programmer is in Python. The extractor serves both now.