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 mathematically prove that code behaves correctly. They catch entire categories of bugs before the code ever runs.

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.

ReasonImpact
Annotation fatigueDevelopers skip contracts when tired or rushed
Time pressureDeadlines trump verification discipline
Maintenance burdenContracts rot when code changes
Learning curveTeams resist unfamiliar syntax
Escape hatchesthrows Exception or catch-all blocks defeat the system

Haskell's Effect System

haskell
-- 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
-- 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
// 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:

C#
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:

Human DevelopersCoding Agents
Find annotation tediousGenerate annotations for free
Forget to update contractsMaintain perfect consistency
Skip verification under time pressureNever cut corners
Resist learning new syntaxAdapt instantly to any syntax
Trade safety for productivitySafety IS productivity

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#
// 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:

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

  §V{v001:User:user} (§C{GetById} id)
  §C{Log} (concat "Retrieved user " (str id))
  §C{CacheSet} user
  §R user
§/F{f001}

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#
// 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 contracts are always enforced:

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

The generated C# includes runtime checks:

C#
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:

Plain Text
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.

Plain Text
§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
§/F{f001}                   //        not declared in §E{db}

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:

Plain Text
┌─────────────────────────────────────────────────────────────┐
│                                                             │
│  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 call chains showing exactly where violations occur
  4. Agent fixes violations with precise information
  5. Repeat until verified

This cycle happens at machine speed. What would take a human team days of debugging completes in seconds.

Real-World Impact

Bug Categories Eliminated

Bug CategoryTraditional DetectionCalor Detection
Undeclared side effectCode review (maybe)Compile error
Missing null checkRuntime NPEContract violation
Invalid state transitionIntegration test (if lucky)Contract violation
Effect leaking through abstractionProduction incidentCompile error with call chain
Contract violationSilent corruptionImmediate, traced exception

Getting Started

To see effect and contract enforcement in action:

Bash
# Compile with enforcement (enabled by default)
calor compile myprogram.calr

# 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 compile myprogram.calr --enforce-effects=false

Learn More