Runtime is proof of ignorance. Every decision deferred to runtime exists because the type system failed to capture it statically.
We formalize the principle that runtime is proof of ignorance: every decision that a program defers to runtime exists precisely because the type system failed to capture it at compile time. The Minimal Runtime Axiom states that the runtime decision set \(\mathcal{R}(P)\) is exactly the complement of the compile-time decidable set \(\mathcal{C}(P)\), where \(\mathcal{C}(P)\) consists of all decisions admitting a static witness \(w_d = (\tau, \pi, \sigma)\)—a type, a proof term inhabiting that type, and a staging certificate guaranteeing the proof is constructible before execution.
We derive three corollaries, develop a full category-theoretic treatment, demonstrate applications to language design through JAPL, and characterize the impossibility boundary through connections to the halting problem, Rice's theorem, and the Self-Reference Incompleteness Principle.
Three fundamental consequences that characterize the structure of runtime decisions.
A decision is legitimately runtime if and only if it depends on \(\omega\)-data: user input, I/O, time, and nondeterminism. Everything else is a failure of static reasoning.
\(|\mathcal{R}(P)|\) is proportional to the epistemic deficit of the type system. More expressive types yield smaller runtime sets—a quantitative metric for language comparison.
Runtime type inspection (reflection, instanceof, typeof) is isomorphic to failure of the Yoneda embedding. A fully characterized value needs no runtime inspection.
Decisions should be transferred as far left as possible. Each arrow represents a decision transfer to an earlier stage.
"Every non-\(\omega\) decision at runtime is a theorem waiting to be proven."