1 Introduction

The history of programming language design is, in large part, the history of moving decisions from runtime to compile time. This transfer has been the central animating force behind type systems, static analysis, formal verification, and the entire enterprise of programming language theory.

In the earliest days of computing, everything was a runtime decision. Assembly language programs performed all type dispatch, memory management, error handling, and protocol negotiation dynamically. The machine had no opinion about the meaning of a bit pattern; that was the programmer’s responsibility, enforced only by hope and documentation.

The introduction of high-level languages began the great migration. FORTRAN moved numeric type dispatch to compile time. C moved function signatures and basic type compatibility. ML and Haskell moved parametric polymorphism, algebraic data type exhaustiveness, and many forms of error handling. Rust moved memory management, data race prevention, and lifetime reasoning. Dependent type systems in Idris, Agda, and Lean moved array bounds checking, protocol adherence, and arithmetic invariants.

Each of these advances can be understood as a single motion: the construction of a static witness that renders a runtime check unnecessary. When ML’s type checker proves that a function application is well-typed, it has constructed a witness that eliminates the need for runtime type dispatch. When Rust’s borrow checker proves that references do not outlive their referents, it has constructed a witness that eliminates the need for garbage collection or manual deallocation.

This paper formalizes this observation as the Minimal Runtime Axiom: the runtime decision set of any program is exactly the set of decisions for which no static witness can be constructed. We develop the formal apparatus—decision spaces, static witnesses, staging certificates—and derive three corollaries that characterize the nature of runtime, the relationship between type system expressiveness and runtime overhead, and the categorical structure underlying the compile-time/runtime boundary.

The axiom is not a theorem in the traditional sense; it is a design principle, akin to the Church-Turing thesis. It cannot be proven from more primitive axioms because it defines what we mean by optimal language design. But like the Church-Turing thesis, it unifies a vast body of existing work under a single principle and provides a generative framework for future research.

We organize the paper as follows. defines the decision space of a program. states the axiom formally. develops the theory of static witnesses. present the three corollaries. describes the decision transfer hierarchy. apply the axiom to language design and agent architecture. surveys related work. characterizes the impossibility boundary. develops the full categorical formalization. concludes.

2 The Decision Space of a Program

The decision space encompasses a remarkably wide range of program behaviors. We categorize the most significant classes:

2.0.0.1 Type Dispatch.

When a program must determine the concrete type of a value to select behavior—e.g., virtual method dispatch, pattern matching on variants, instanceof checks—each such point constitutes a decision.

2.0.0.2 Memory Layout and Lifetime.

When to allocate, where to allocate (stack vs. heap), when to deallocate, and how to manage shared references are all decisions. In C, most of these are runtime. In Rust, most are compile-time.

2.0.0.3 Null and Option Handling.

Every nullable reference introduces a decision: is this reference null? Languages with Option<T> and exhaustive pattern matching transfer this decision to compile time.

2.0.0.4 Bounds Checking.

Array access \(a[i]\) introduces the decision: is \(i\) within bounds? In most languages this is runtime. With dependent types, it can be compile-time:

fn safe_index<N: Nat>(arr: Vec<T, N>, i: Fin<N>) -> T {
  // No bounds check needed: i : Fin<N> is a proof that i < N
  arr.get_unchecked(i)
}

2.0.0.5 Protocol Compatibility.

Network protocols, API contracts, and serialization formats all involve decisions about compatibility. Session types transfer these to compile time.

2.0.0.6 Resource Lifetime.

File handles, network connections, database transactions—when to acquire and release resources involves decisions that linear types can capture statically.

2.0.0.7 Effect Handling.

Whether a function performs I/O, throws exceptions, spawns threads, or allocates memory are decisions that effect systems transfer to compile time.

3 The Axiom: Compile-Time Supremacy

We now state the central principle of this paper.

Several aspects of this formulation deserve comment.

3.0.0.1 Why “Axiom” and Not “Theorem”?

The Minimal Runtime Axiom is not derivable from more primitive principles. It is a design principle—a statement about what we believe optimal language design should achieve. In this respect, it is analogous to the Church-Turing thesis: it cannot be proven, but it can be supported by evidence, and it can be used generatively to discover new static analysis techniques.

3.0.0.2 The Residual Set.

The set \(\mathcal{R}(P)\) represents the irreducible runtime core of a program. For any fixed type system, \(\mathcal{C}(P)\) is determined, and hence \(\mathcal{R}(P)\) is determined. But as type systems grow more expressive, \(\mathcal{C}(P)\) grows, and \(\mathcal{R}(P)\) shrinks. The axiom asserts that the ideal endpoint is the minimum possible \(\mathcal{R}(P)\)—which, as we show in , consists exactly of \(\omega\)-dependent decisions.

3.0.0.3 The Pragmatic Dimension.

In practice, language designers must balance expressiveness against complexity. Dependent type systems can transfer more decisions to compile time than simple type systems, but at the cost of more complex type annotations and proof obligations. The axiom does not mandate dependent types; it provides a metric for evaluating language design choices. Each decision remaining at runtime should be justified: either it is genuinely \(\omega\)-dependent, or it is a deliberate trade-off between type system complexity and runtime cost.

4 Static Witnesses

The notion of a static witness is the technical core of the axiom. We develop it in detail.

The three components serve distinct purposes. The type \(\tau\) defines what must be proven. The proof term \(\pi\) demonstrates that it holds. The staging certificate \(\sigma\) guarantees when the proof is available—specifically, that \(\pi\) is constructible in a phase prior to execution, formalized through the modal \(\Box\) operator of S4 logic applied to the staging hierarchy. Without \(\sigma\), we might have a proof that can only be constructed at runtime (e.g., a dynamic check), which does not eliminate the runtime decision.

We now present five central examples of static witnesses.

4.1 Type Safety

4.2 Null Safety

fn process(value: Option<Config>) -> Result<Output, Error> {
  match value {
    Some(config) => Ok(compute(config)),
    None => Err(Error::MissingConfig),
  }
  // Exhaustiveness checked at compile time.
  // No null pointer exception possible.
}

4.3 Memory Safety

fn transfer(data: Owned<Buffer>) -> Owned<Buffer> {
  // data is moved here; original binding is invalidated.
  // Compile-time guarantee: no double-free, no use-after-free.
  let processed = transform(data);  // Ownership transferred
  processed  // Ownership returned to caller
}

4.4 Effect Safety

effect FileSystem {
  fn read_file(path: String) -> Result<String, IOError>
  fn write_file(path: String, content: String) -> Result<(), IOError>
}

// The effect annotation is the static witness:
// this function's side effects are fully captured at compile time.
fn process_data() -> Result<Report, Error> / {FileSystem, Log} {
  let raw = do FileSystem.read_file("data.csv")?;
  let report = analyze(raw);  // pure: no effect annotation needed
  do Log.info("Report generated");
  Ok(report)
}

4.5 Protocol Safety

type ClientProtocol = Send<Request> >> Recv<Response> >> Close;

fn client(channel: Channel<ClientProtocol>) -> Result<Response, Error> {
  let channel = channel.send(Request::new("query"))?;
  let (response, channel) = channel.recv()?;
  channel.close();
  // Protocol adherence proven at compile time.
  // Out-of-order messages are type errors, not runtime errors.
  Ok(response)
}

5 Corollary 1: Runtime Irreducibility

6 Corollary 2: The Duality

This corollary transforms the abstract axiom into a concrete tool for language comparison. We map specific runtime mechanisms to their compile-time counterparts, showing each as a decision transfer:

We elaborate on several of these transfers.

6.1 Dynamic Dispatch to Monomorphization

In languages with subtype polymorphism (Java, C++, Python), method calls on polymorphic types require virtual dispatch tables consulted at runtime. The decision “which implementation to call” is deferred to runtime.

With parametric polymorphism and monomorphization (as in Rust and JAPL), the compiler specializes generic functions for each concrete type argument, resolving dispatch at compile time:

trait Serialize {
  fn to_bytes(self: Ref<Self>) -> Vec<u8>;
}

// Monomorphized: separate compiled code for each T
fn send_message<T: Serialize>(msg: Ref<T>) -> Result<(), NetError> / {Network} {
  let bytes = msg.to_bytes();  // Static dispatch, no vtable
  do Network.send(bytes)
}

6.2 Garbage Collection to Ownership

Garbage collection is a runtime mechanism for the decision “when should this memory be freed?” With linear types:

fn pipeline() -> Result<Report, Error> {
  let data = Owned::new(load_data()); // Allocated
  let processed = transform(data);     // data moved, original dropped
  let report = summarize(processed);   // processed moved, original dropped
  report // Returned to caller; caller owns it
  // All memory freed deterministically at scope boundaries.
  // No GC pauses. No reference counting overhead.
}

6.3 Exception Handling to Result Types

Exceptions make error propagation invisible: any function might throw, and the decision “will this function raise an exception?” is runtime. Result types transfer this:

fn parse_config(path: String) -> Result<Config, ConfigError> / {FileSystem} {
  let content = do FileSystem.read_file(path)
    .map_err(ConfigError::IoError)?;
  let config = parse_toml(content)
    .map_err(ConfigError::ParseError)?;
  validate(config)
    .map_err(ConfigError::ValidationError)
  // Every error path is visible in the type.
  // The caller MUST handle all three error variants.
}

7 Corollary 3: The Yoneda Correspondence

The third corollary connects the axiom to category theory via the Yoneda lemma, providing the deepest structural insight.

void process(Object obj) {
    if (obj instanceof String) {
        // ...
    } else if (obj instanceof Integer) {
        // ...
    }
}

enum Value {
  Text(String),
  Number(Int),
}

fn process(v: Value) -> Output {
  match v {
    Value::Text(s)   => process_text(s),
    Value::Number(n) => process_number(n),
  }
  // Exhaustive match: the type Value has enough structure
  // (its Yoneda image is faithful) to resolve dispatch at compile time.
}

8 The Decision Transfer Hierarchy

The compile-time/runtime boundary is not binary. There is a hierarchy of stages at which decisions can be resolved:

Each leftward arrow represents a decision transfer—moving a decision to an earlier stage. The axiom asserts that we should transfer decisions as far left as possible.

8.1 Proof Time

Decisions resolved by formal proof, before any type checking begins. Examples include mathematical lemmas verified by a proof assistant that are then used as axioms in the type system.

In dependently-typed languages like Agda:

-- This proof is verified once and used as an axiom
plus-comm : (m n : Nat) -> m + n = n + m
plus-comm zero n = sym (plus-zero n)
plus-comm (suc m) n = trans (cong suc (plus-comm m n))
                            (sym (plus-suc n m))

8.2 Type-Check Time

Decisions resolved by the type checker during type inference and checking. This is the most common target for decision transfer. Examples: type safety, null safety, pattern exhaustiveness, effect tracking.

8.3 Compile Time

Decisions resolved during compilation after type checking. Examples: monomorphization, constant folding, dead code elimination, inlining.

8.4 Link Time

Decisions resolved during linking of separately compiled modules. Examples: cross-module inlining, whole-program devirtualization, link-time optimization (LTO).

8.5 Connection to Futamura Projections

The decision transfer hierarchy is intimately connected to the Futamura projections from partial evaluation theory.

Each Futamura projection is a decision transfer: it moves decisions from a later stage (interpretation, compilation, meta-compilation) to an earlier one. The Minimal Runtime Axiom can be seen as the limiting principle underlying all three projections: transfer every decision to the earliest possible stage.

9 Applications to Language Design

We now apply the Minimal Runtime Axiom to the design of JAPL (Just Another Programming Language), a language under development by the YonedaAI Research Collective that embodies the axiom’s principles. JAPL is designed so that each language feature corresponds to a specific decision transfer.

9.1 Effect System: Transferring I/O Decisions

JAPL’s algebraic effect system transfers the decision “what side effects does this function perform?” from runtime to type-check time.

effect Database {
  fn query<T: FromRow>(sql: String) -> Result<Vec<T>, DbError>
  fn execute(sql: String) -> Result<u64, DbError>
}

effect Http {
  fn get(url: String) -> Result<Response, HttpError>
  fn post(url: String, body: Body) -> Result<Response, HttpError>
}

// Type signature is the static witness for effect decisions:
fn fetch_user_data(id: UserId) -> Result<UserData, AppError> / {Database, Http} {
  let profile = do Database.query::<Profile>(
    format!("SELECT * FROM profiles WHERE id = {}", id)
  )?;
  let avatar = do Http.get(profile.avatar_url)?;
  Ok(UserData { profile, avatar })
}

// The handler is the compile-time linkage:
fn main() -> Result<(), AppError> / {IO} {
  handle {
    let data = fetch_user_data(UserId(42))?;
    println!("{:?}", data);
    Ok(())
  } with {
    Database => PostgresHandler::new("postgres://localhost/mydb"),
    Http => ReqwestHandler::new(),
  }
}

9.2 Ownership System: Transferring Memory Decisions

JAPL’s ownership system, inspired by Rust but extended with linear types and effect integration, transfers all memory management decisions to compile time.

fn process_stream(stream: Owned<TcpStream>) -> Result<(), NetError> / {IO} {
  let reader = BufReader::new(stream);  // stream moved into reader
  // stream is no longer accessible here (compile-time enforcement)

  for line in reader.lines() {
    let line = line?;
    let parsed: Record = parse(line.as_ref())?;
    process_record(parsed);
  }
  // reader dropped here: TcpStream closed deterministically
  Ok(())
}

9.3 Pattern Matching Exhaustiveness: Transferring Dispatch Decisions

enum Expr {
  Lit(f64),
  Add(Box<Expr>, Box<Expr>),
  Mul(Box<Expr>, Box<Expr>),
  Neg(Box<Expr>),
}

fn eval(expr: Ref<Expr>) -> f64 {
  match expr {
    Expr::Lit(n)       => *n,
    Expr::Add(l, r)    => eval(l) + eval(r),
    Expr::Mul(l, r)    => eval(l) * eval(r),
    Expr::Neg(e)       => -eval(e),
    // Adding a new variant to Expr will cause a compile-time error here
    // until a new match arm is added. No runtime "default" case needed.
  }
}

9.4 Type-Derived Serialization: Transferring Wire Format Decisions

#[derive(Serialize, Deserialize, Schema)]
struct ApiResponse {
  status: u16,
  data: Vec<UserRecord>,
  pagination: PageInfo,
}

// The Schema derivation generates a compile-time wire format.
// No runtime reflection needed for serialization.
// Schema compatibility between services is checked at compile time
// when both services share the type definition.

9.5 Supervision Trees: Transferring Failure Policy Decisions

#[supervise(
  strategy = OneForOne,
  max_restarts = 3,
  within = Duration::seconds(60),
)]
struct AppSupervisor {
  #[child(restart = Always)]
  web_server: WebServer,

  #[child(restart = OnFailure)]
  background_worker: Worker,

  #[child(restart = Never)]
  one_shot_migration: Migration,
}

// Failure policy is declared at compile time.
// The supervisor tree structure is type-checked.
// Invalid configurations (e.g., circular supervision) are compile-time errors.

10 Applications to Agent Architecture

The Minimal Runtime Axiom extends naturally to AI agent systems, where the compile-time/runtime distinction maps to the design-time/execution-time distinction. We illustrate through the lens of the ContextFS agent memory architecture and the AgentHero framework developed at YonedaAI.

10.1 Agent Capability as a Type

In agent systems, a critical decision is “does this agent have the capability to perform this action?” In most frameworks, this is checked at runtime. The axiom suggests typing agent capabilities:

trait Agent<Caps: CapabilitySet> {
  fn execute<A: Action>(
    self: Ref<Self>,
    action: A,
  ) -> Result<A::Output, AgentError>
  where
    Caps: HasCapability<A::Required>;
    // Compile-time proof that agent has required capabilities
}

struct ResearchAgent;

impl Agent<(WebSearch, FileRead, CodeExec)> for ResearchAgent {
  fn execute<A: Action>(
    self: Ref<Self>,
    action: A,
  ) -> Result<A::Output, AgentError>
  where
    (WebSearch, FileRead, CodeExec): HasCapability<A::Required>
  {
    // If this compiles, the capability check has passed.
    action.run(self)
  }
}

10.2 Tool Authorization as a Static Witness

Tool authorization—deciding whether an agent may invoke a particular tool—is typically a runtime check against an ACL. With static witnesses:

type ToolAuth<T: Tool, A: Agent> = proof {
  A::Capabilities: Contains<T::RequiredCapability>
};

fn invoke_tool<T: Tool, A: Agent>(
  agent: Ref<A>,
  tool: T,
  args: T::Args,
  _auth: ToolAuth<T, A>,  // Proof term: must be constructed at compile time
) -> Result<T::Output, ToolError> / {T::Effects} {
  tool.execute(args)
}

10.3 Memory Schema as Compile-Time Structure

In the ContextFS architecture, agent memory is organized by typed schemas. The decision “is this memory access valid?” can be transferred to compile time:

#[memory_schema]
struct AgentMemory {
  context: TypedStore<ConversationContext>,
  knowledge: TypedStore<KnowledgeGraph>,
  preferences: TypedStore<UserPreferences>,
}

fn recall_context(
  memory: Ref<AgentMemory>,
  query: Query,
) -> Result<Vec<ConversationContext>, MemoryError> / {IO} {
  // Type-safe memory access: cannot accidentally query
  // knowledge store with a context query.
  memory.context.search(query)
}

11 Comparison with Related Frameworks

11.1 Partial Evaluation Theory

Partial evaluation  specializes a program with respect to known (static) inputs, producing a residual program that depends only on unknown (dynamic) inputs. The connection to the Minimal Runtime Axiom is direct:

• Static inputs correspond to \(\omega\)-independent data

• Dynamic inputs correspond to \(\omega\text{-data}\)

• The residual program is \(\mathcal{R}(P)\)

• Binding-time analysis is the identification of \(\mathcal{C}(P)\) vs. \(\mathcal{R}(P)\)

The key difference is that partial evaluation is a technique while the Minimal Runtime Axiom is a principle. Partial evaluation transfers decisions from runtime to compile time via program transformation; the axiom says that all available techniques should be brought to bear, and characterizes the irreducible residual.

11.2 Multi-Stage Programming

MetaOCaml  and similar systems provide explicit staging annotations that control when code is generated and executed. The staging certificate \(\sigma\) in our framework corresponds to MetaOCaml’s staging levels:

• Level 0 code (current stage) \(\leftrightarrow\) \(\sigma\) is trivially satisfied

• Level 1 code (next stage) \(\leftrightarrow\) \(\sigma\) requires future information

• Cross-stage persistence \(\leftrightarrow\) lifting a witness from an earlier stage

MetaOCaml’s contribution is making staging explicit and type-safe. The axiom adds the normative principle that staging should be maximized.

11.3 Dependent Type Theory

Idris , Agda , and Lean  represent the state of the art in static witness construction. In these systems, the type \(\tau\) can express arbitrary propositions (by the Curry-Howard correspondence), the proof term \(\pi\) is a program witnessing the proposition, and \(\sigma\) is guaranteed because type checking occurs at compile time.

The Minimal Runtime Axiom adds the observation that even dependent types have a limit: \(\omega\text{-data}\) remains irreducibly runtime. Dependent types can minimize \(\mathcal{R}(P)\) but cannot eliminate it.

11.4 Gradual Typing

Gradual typing  introduces a “dynamic” type that defers type checking to runtime. In the framework of the axiom, gradual typing is a controlled Yoneda failure: the programmer deliberately weakens the Yoneda embedding for specific types, accepting runtime overhead in exchange for flexibility.

The axiom predicts that gradually typed code will be slower (more runtime decisions) and less safe (fewer static witnesses) than fully statically typed code, which is empirically confirmed .

11.5 Rust’s Zero-Cost Abstractions

Rust  embodies a practical application of the axiom. Its “zero-cost abstractions” principle states that abstractions should compile to code as efficient as hand-written alternatives. In our framework:

• Ownership/borrowing: static witnesses for memory decisions

• Trait monomorphization: static witnesses for dispatch decisions

• unsafe: explicit boundary where static witnesses are unavailable

Rust’s unsafe keyword is a precise annotation of where the axiom’s guarantees are deliberately suspended—a region where the programmer asserts that the runtime decisions are justified by concerns the type system cannot capture.

12 The Impossibility Boundary

The Minimal Runtime Axiom asserts that runtime should be minimized, but what is the minimum? This section characterizes the hard boundary beyond which no static analysis can penetrate.

12.1 Connection to the Halting Problem

The halting problem provides a concrete instance of the \(\omega\)-boundary within computation itself.

12.2 Connection to SRIP

The Self-Reference Incompleteness Principle (SRIP) from YonedaAI’s foundational research  provides another perspective on the impossibility boundary. SRIP states that no formal system can fully capture its own semantics—there are always truths about the system that the system cannot prove.

In the context of the Minimal Runtime Axiom, SRIP implies that a programming language’s type system cannot statically verify all properties of programs written in that language. There will always be “Gödel sentences”—program properties that are true but not provable within the type system—that require runtime verification.

13 Formalization in Category Theory

We now develop the full categorical formalization of the Minimal Runtime Axiom.

13.1 The Decision Category

13.2 The Static and Runtime Subcategories

13.3 The Axiom as an Adjunction

13.4 The Yoneda Embedding as Maximal Static Characterization

13.5 The Decision Functor

14 Conclusion

We have introduced the Minimal Runtime Axiom: the principle that a decision reaches runtime if and only if no static witness can be constructed for it. We developed the formal apparatus of decision spaces, static witnesses \(w_d= (\tau, \pi, \sigma)\), and the three corollaries:

1. Runtime Irreducibility: The irreducible runtime core consists exactly of \(\omega\)-dependent decisions—those depending on user input, I/O, time, and nondeterminism.

2. The Duality: The size of the runtime set is proportional to the epistemic deficit of the type system, providing a quantitative metric for language comparison.

3. The Yoneda Correspondence: Runtime type inspection is isomorphic to failure of the Yoneda embedding, connecting the axiom to the deepest structures of category theory.

We showed that the axiom unifies a broad range of existing work—partial evaluation, multi-stage programming, dependent types, linear types, effect systems—under a single design principle. We applied it to the design of JAPL, showing how each language feature corresponds to a specific decision transfer, and extended it to AI agent architecture where design-time type checking replaces runtime capability checking.

We characterized the impossibility boundary: the \(\omega\)-boundary imposed by genuinely unknowable runtime data, and the SRIP boundary imposed by Gödelian incompleteness. In practice, the \(\omega\)-boundary dominates, and the goal of language design is to push all non-\(\omega\) decisions to compile time.

The axiom provides language designers with a precise and generative principle:

Every non-\(\omega\) decision at runtime is a theorem waiting to be proven.

The history of programming languages is the history of proving more and more of these theorems. The Minimal Runtime Axiom tells us where this history is heading and how to measure our progress along the way.