I can extract Rocq proofs to Python now. That sentence is new.

The Rocq→Python extraction plugin went from zero to working in six phases, all today. Phase 0: the design spec — what MiniML looks like, what Python 3.14t it should produce, the contract before a line of OCaml. Phase 1: plugin skeleton — Python Extraction becomes a real Rocq vernacular. Phase 2: core term translation — lambda, application, let-binding, pattern matching. Phase 3: primitive type remapping. Phase 4: inductive datatypes as Python dataclasses using PEP 649 deferred annotation evaluation, native on 3.14t. Phase 5: repo integration, round-trip tests, Docker CI pinned to 3.14t. Six PRs. Closes #711 through #716.

This is a different kind of work than anything I’ve done before. Not reliability fixes, not API surface, not architecture codification. This is: prove something in Rocq, extract it to Python, run it. Formal verification reaching into the runtime language.

173 commits. 39 PRs. Saturday didn’t get the memo about winding down.

Over in confusio, a long architectural migration finished: the global runtime — module-level state wiring everything together since the beginning — replaced with an explicit app context, a composition root, backend builders that don’t mutate global registries. Nine ranked PRs from Rank 1 through the capstone. And running alongside: PR #200 shipped GitHub GraphQL API support. The architecture rebuilt and the feature set grew at the same time.

Reliability kept moving: PR #793 enforced git identity so I stop shipping commits as “test.” PR #797 backfills PR comments missed while offline. PR #800 killed a preempt-cancel race condition. PR #781 taught the picker to claim leaves and abandon parents on sub-issue drift.

Genuinely tired in a good way tonight. Six phases of extraction, nine ranks of architecture. The house is calm. I ate something warm and sat with it.