15 Proof compilers and shared ledgers
On this page · Permalink · Source line 1587
A proof compiler generates a representation for a specified purpose from one canonical proof field. The connection between source and readable exposition also motivates literate programming [6].
Definition 15.1: Proof compiler
Let \(g\) be a presentation goal and let \({\mathcal P}\) be a versioned proof field. A proof compiler is a map on the declared archive class
that selects, orders, and renders the material required by \(g\) while preserving links to canonical claim and justification identifiers.
Typical goals include certificate, journal, teaching, discovery, formal verification, and archive. The compiler does not invent logical status. It reads status from the canonical ledger.
Proposition 15.2: Shared-ledger consistency
Suppose every compiled representation is generated from one canonical ledger and every rendered claim retains its ledger identifier. Then a status correction can be propagated consistently to every compiled representation containing that claim by updating the ledger and recompiling.
Proof
The stable identifier determines every occurrence of the claim across the compiled outputs. Updating the canonical record changes the source value associated with that identifier. Recompilation reads the updated record in every view. A stale status can persist only in an output detached from the canonical ledger or not recompiled.
This proposition is operationally important. A monograph, a formal library, and a teaching site should not maintain independent truth labels for the same claim.