The Verification Opportunity

Why effects and contracts enforcement is only practical in coding agent languages—and why this changes everything.

The 50-Year Struggle

Computer scientists have known since the 1970s how to make software more reliable:

• Effect Systems: Track side effects at compile time (Gifford & Lucassen, 1986)
• Design by Contract: Specify preconditions and postconditions (Meyer, 1986)
• Dependent Types: Encode invariants in the type system (Martin-Löf, 1972)

These techniques can prove specific obligations inside a precisely modeled surface. They do not prove that an entire program is correct. When Calor cannot make a clean proof, it reports why and keeps the runtime check.

So why isn't all software written this way?

Why Humans Don't Write Annotations

Every attempt to bring verification to mainstream programming has hit the same wall: human annotation burden.

Haskell's Effect System

-- Haskell requires effect annotations everywhere
readFile :: FilePath -> IO String
writeFile :: FilePath -> String -> IO ()

-- Every function that uses IO must declare it
processConfig :: FilePath -> IO Config
processConfig path = do
    contents <- readFile path  -- Forces IO in type signature
    return (parseConfig contents)

Result: Haskell remains a niche language. Most programmers find the discipline too burdensome for everyday work.

Eiffel's Design by Contract (1986)

-- Eiffel requires manual contract annotation
deposit (amount: INTEGER)
    require
        positive_amount: amount > 0
        account_open: is_open
    do
        balance := balance + amount
    ensure
        balance_increased: balance = old balance + amount
    end

Result: Eiffel never achieved mainstream adoption. The annotation overhead was too high for most development teams.

Java's Checked Exceptions

// Java forces you to declare every exception
public void processFile(String path) throws IOException, ParseException {
    String content = Files.readString(Path.of(path));  // throws IOException
    parse(content);  // throws ParseException
}

Result: Developers circumvent the system with throws Exception or catch-all blocks. The signal is lost.

C# Code Contracts (2008-2015)

Microsoft introduced Code Contracts for .NET—a promising approach to design-by-contract:

public int Divide(int a, int b)
{
    Contract.Requires(b != 0);
    Contract.Ensures(Contract.Result<int>() * b == a);
    return a / b;
}

Result: Abandoned by Microsoft. The static analyzer was slow, the runtime overhead was significant, and developers simply didn't write contracts consistently enough to justify the tooling investment.

Why AI Agents Change Everything

Coding agents change this equation fundamentally:

When an agent writes code, the annotation cost is zero.

This isn't incremental improvement. It's a phase transition that makes previously impractical techniques suddenly viable.

C# vs Calor: What's Different

Problem 1: Hidden Side Effects

In C#, function signatures don't reveal their side effects:

// C#: What effects does this function have?
public async Task<User> GetUser(int id)
{
    var user = await _repository.GetById(id);  // Database? Memory?
    _logger.Log($"Retrieved user {id}");        // Console? File? Network?
    await _cache.Set(user);                      // Memory? Redis?
    return user;
}
// Answer: You have NO IDEA without reading every dependency

In Calor, effects are explicit in the signature:

§F{f001:GetUser:pub}
  §I{i32:id}
  §O{User}
  §E{db,cw,net}                    // EXPLICIT: database, console write, network

  §B{user:User} §C{GetById} §A id §/C
  §C{Log} (concat "Retrieved user " (str id))
  §C{CacheSet} user
  §R user

An agent (or human) reading this function knows immediately:

• It accesses a database
• It writes to the console
• It uses the network

No guessing. No reading implementation details. No surprises.

Problem 2: Contracts That Disappear

C# offers Debug.Assert, but these vanish in release builds:

// C#: These contracts vanish in release builds
public static int Divide(int a, int b)
{
    Debug.Assert(b != 0, "Divisor cannot be zero");  // GONE in Release
    return a / b;
}
// In production: DivideByZeroException with no context

Calor preconditions are emitted as runtime checks unless contract checks are explicitly disabled with --contract-mode off. For supported body shapes, postconditions are emitted unless optional --verify produces an eligible, clean, non-vacuous proven result. Inconclusive results do not authorize proof-based removal; they do not guarantee that runtime lowering is supported. See verification modes and limits.

§F{f001:Divide:pub}
  §I{i32:a}
  §I{i32:b}
  §O{i32}
  §Q{message="divisor must not be zero"} (!= b 0)
  §R (/ a b)

The generated C# includes runtime checks:

public static int Divide(int a, int b)
{
    if (!(b != 0))
        throw new ContractViolationException(
            "Precondition failed: divisor must not be zero",
            functionId: "f001",
            kind: ContractKind.Requires,
            line: 5);
    return a / b;
}

Interprocedural Analysis

Calor doesn't just check individual functions. It analyzes the entire call graph:

error Calor0410: Function 'ProcessOrder' uses effect 'network'
                 but does not declare it
  Call chain: ProcessOrder → NotifyCustomer → SendEmail → HttpClient.PostAsync

The compiler traces effect violations through any depth of calls. You can't hide a side effect by burying it in helper functions.

§F{f001:ProcessOrder:pub}
  §I{Order:order}
  §O{bool}
  §E{db}                    // Declares: only database effects

  §C{SaveOrder} order       // OK: SaveOrder has db effect
  §C{SendEmail} order       // ERROR: SendEmail has net effect

The compiler catches this. Not a linter warning. Not a code review comment. A hard error that blocks compilation.

The Virtuous Cycle

When agents both write and verify code, a powerful feedback loop emerges:

┌─────────────────────────────────────────────────────────────┐
│                                                             │
│  Agent generates code  ───►  Compiler verifies effects     │
│         ▲                           │                       │
│         │                           ▼                       │
│  Agent fixes violations  ◄───  Errors with call chains     │
│                                                             │
└─────────────────────────────────────────────────────────────┘

1. Agent generates code with effect declarations and contracts
2. Compiler verifies effects are properly declared
3. Errors include resolved call chains when the analysis can recover them
4. Agent fixes violations with precise information
5. Repeat until checks pass and the remaining assumptions are reviewed

This shortens the feedback loop while keeping unresolved boundaries visible to the reviewer.

Real-World Impact

Bug Categories Surfaced Earlier

The nullability guide defines Calor 0.22's bounded support. It does not promise whole-program null safety: mutable assignment/rebinding and constructor-input enforcement remain excluded. Missing interop annotations (Oblivious) are conservatively possibly null; available annotations are trusted, not proved. Type/effect controls and transpile-only do not bypass active binding checks.

These checks are separate from contract proof. D3 nullability, D12 string indexing/counting semantics, and D14 reference-model limits still require verifier proof demotions and retained runtime guards. #875 remains open. A bounded regression set is not a universal safety result; see Verification Guarantees and Limits.

Getting Started

To see effect and contract enforcement in action:

# Compile with enforcement (enabled by default)
calor --input myprogram.calr --output myprogram.g.cs

# See effect violations with call chains
# error Calor0410: Function 'f001' uses effect 'console_write' but does not declare it

# Disable for migration (not recommended)
calor --input myprogram.calr --output myprogram.g.cs --no-enforce-effects

Learn More

• Effects Reference - Complete effect syntax and available effect types
• Contracts Reference - Precondition and postcondition syntax
• Verification Guarantees - Proof outcomes, modeled forms, and runtime-check retention
• Design Principles - The five principles behind Calor