Nestor G Pestelos Jr · Writing · Print

When AI Writes Code, Types Become the Proof Harness

Published October 11, 2026

TL;DR

Static typecheckers check encoded constraints; formal proof verifiers check stated propositions under explicit assumptions. Both can bound AI search, while humans remain responsible for the specification and behavior those checks do not cover.

A common reaction to modern AI coding assistants is that static type safety has become obsolete. If an LLM can generate boilerplate instantly and infer shapes on the fly, why bother with strict type systems, compiler rituals, and formal annotations? Why not let Python, JavaScript, and Ruby dominate while the model fills in the gaps?

This reaction mistakes authoring convenience for system verification.

When a human writes code, static typing can feel like friction: you stop to satisfy the compiler. When an AI writes code, human attention can become the scarce resource. If an LLM generates 500 lines of dynamically typed code, reviewers still need evidence about branches, variable references, and runtime assumptions. Tests and static analysis can check some of these; human review covers the remaining risks.

For autonomous AI agents, static types provide an automated verification harness that bounds probabilistic search.

1. The Verification Asymmetry

The Bitter Lesson of computing applies to AI-assisted software engineering. Paras Chopra formulated the modern economic rule behind scaling laws:

"if a good solution can be verified cheaply, scale will dominate cleverness"

Where verification is cheap and automated, you can generate candidate rollouts and keep only the ones that pass. This generate-and-check strategy becomes harder to scale when verification is expensive or ambiguous.

In 2x, not 10x: coding with LLMs in 2026, O’Bryant proposes that reliable automated feedback explains much of the gain he has observed. He identifies maintainability and documentation judgment as remaining limits. This is a hypothesis based on his own experience.

Both dynamic and statically typed programs need runtime tests for behavior outside static checks. A static typechecker adds automated checks of type constraints before execution. Their cost depends on the language, configuration, and codebase.

2. Programs as Proofs: The Curry-Howard Foundation

The Curry-Howard correspondence relates propositions to types and proofs to programs in suitable formal calculi. Prabhakar Ragde details this connection in Logic and Computation Intertwined:

In a proof assistant, an LLM can synthesize a proof term for a stated proposition. A mainstream typed function usually carries a narrower contract, such as its input and output types. Passing its typechecker does not prove that the function implements the intended algorithm.

       Logic (Propositions)       <--->      Computation (Types)
   ─────────────────────────────────────────────────────────────
   Proposition A                   <--->      Data Type A
   Conjunction (A ∧ B)             <--->      Product Type (Pair A B)
   Disjunction (A ∨ B)             <--->      Sum Type (Either A B)
   Implication (A → B)             <--->      Function Type (A -> B)
   Universal Proof (∀ x:A. B(x))   <--->      Dependent Function (Π-Type)
   Proof Verification              <--->      Type Checking

Proof assistants such as Agda, Coq, and Lean use dependent types to express propositions and check proof terms. When an AI generates a proof in Lean, the kernel checks it against the stated proposition. The result depends on the axioms and assumptions used, as the Lean documentation explains.

Alon and eight coauthors present a digested, human-verified version of OpenAI’s unit-distance counterexample. Their work combines human checking and explanation of a machine-generated result.

Formal verification can establish that an artifact satisfies a stated proposition under its assumptions before a human can explain the proof.

Human understanding still supports teaching and extending results. In a collective declaration posted by Terence Tao on 20260911, Fields Medallists describe how talks, discussions and simplification turn results into textbook material. They stress that work with students develops their ability to pursue new ideas, and warn that mass production of results may erode this human transmission chain.

When an LLM generates a type error in a dynamically typed language, it may remain undetected until execution. A function receives nil instead of a string, or an object missing a required attribute, and the program crashes three stack frames away at runtime.

A static typechecker can catch mismatches represented in its type rules before the code runs. Consider an agent implementing a payment state transition. In dynamically typed code, an agent can accidentally transition a Failed payment to Refunded:

# This invalid state transition can pass without an exception.
def process_refund(payment):
    payment.status = "refunded"
    gateway.send_refund(payment.id, payment.amount)

In a language using the typestate pattern, states are distinct types, making invalid transitions unrepresentable:

// Static: compiler rejects invalid state transition at compile time
struct SettledPayment { id: String, amount: u64, receipt: Receipt }
struct FailedPayment  { id: String, reason: String }

fn process_refund(payment: SettledPayment) -> RefundReceipt { ... }

When an agent passes a FailedPayment to process_refund, the Rust compiler reports a type mismatch:

error[E0308]: mismatched types
  --> src/checkout.rs:42:25
   |
42 |     process_refund(payment);
   |                    ^^^^^^^ expected `SettledPayment`, found `FailedPayment`

This diagnostic identifies a mismatch with the encoded state constraint. An autonomous coding agent can use it to adjust the implementation and retry. It does not establish that the refund amount or gateway behavior is correct.

4. The Two Hard Limits of Type Safety

A. Type Safety Is Not Semantic Correctness

Gergely Orosz disputes claims that agentic code is error-free. He argues that it remains buggy and can introduce errors and vulnerabilities that are harder to spot.

A program can satisfy its type constraints and memory-safety rules while computing the wrong tax calculation, discarding user data, or causing race conditions in external services. Static guarantees cover properties represented in the type system, subject to its soundness and assumptions.

B. The Specification Inversion Trap

Based on what he hears and sees, Nate Berkopec reports that many people review model-generated application code more closely than generated tests. He suspects verification and specification should receive more attention than implementation.

The same inversion threatens type-driven development. If an engineer asks an LLM to generate both the complex type signatures and the implementation, the LLM can define trivial or tautological types that type-check while asserting nothing of value. A sound checker can confirm a weak or incorrect specification. Humans must review what the specification claims, as well as whether the implementation passes.

5. The Spectrum of Practical Verification

Adopting formal verification for AI generation does not require writing every web application in Coq or Agda. In practice, type safety exists along an expressiveness spectrum:

  1. Mainstream Structural Safety (TypeScript, Go): Catches many shape mismatches, missing fields, and typo bugs. Coverage varies by language and configuration. TypeScript deliberately permits some unsound operations, so a passing check is not a proof of runtime safety.
  2. Algebraic Invariant Typing (Rust, Haskell): Algebraic data types and pattern matching can encode states and expose unhandled cases. Rust also uses ownership rules to prevent data races in safe Rust. These guarantees depend on the encoded model and language rules; Haskell does not share Rust's ownership model.
  3. Dependent Type Theory (Lean 4, Agda, Idris): Can encode mathematical propositions, array bounds, and state transition certificates in types. Proof checking establishes the encoded claim under the selected assumptions; it does not validate unstated intent.

More expressive specifications can check more properties, but they also require work to write and validate.

The New Engineering Division of Labor

AI coding gives developers another division of labor: define types and boundary specifications, let the model generate candidate implementations, and use automated checks to reject candidates that violate those constraints.

Humans must still validate the specification, review behavior outside the checks, and understand enough of the result to maintain and extend it. Typecheckers and proof verifiers reduce the review burden within their scope; they cannot guarantee that an unstated requirement has been met.

Sources

Back to top