Philosophy

AI coding agents are transforming software development, but they're forced to work with languages designed for humans. This creates a fundamental mismatch.

The Core Insight

When an AI agent reads code, it needs answers to specific questions:

Traditional languages make agents infer these answers through complex analysis. Calor makes them explicit in the syntax.

The Verification Advantage

"Why not just use constrained decoding?"

Tools like LLGuidance can constrain LLM output to valid syntax. If an AI can already generate syntactically correct C#, why use Calor?

Because syntax correctness ≠ semantic correctness.

What Constrained Decoding Can't Catch

// LLGuidance-constrained C# — syntactically perfect, semantically buggy
public int Divide(int a, int b) {
    return a / b;  // Compiles fine. Crashes on b=0.
}

// Calor — Z3 catches the bug at compile time
§F{f001:Divide:pub} (i32:a, i32:b) -> i32
  §E{}
  §Q (!= b 0)          // ← Contract: b must not be zero
  §S (>= result 0)     // ← Contract: result non-negative
  §R (/ a b)

Calor's Z3 integration classifies each obligation. Supported obligations may be proven or refuted with a counterexample; incomplete modeling is reported as assumed, unknown, timeout, unsupported, or unavailable. Only a clean, non-vacuous proof can remove an emitted runtime check.

Verification-First, Agent-Friendly Second

Calor is a verification-first language that happens to be agent-friendly—not just an "agent DSL." The explicit syntax serves verification: contracts in a structured format can be parsed and proven by Z3.

The v0.12 static benchmark reports:

• 1.49x Error Detection — more explicit detection signals under the calculator
• 1.84x Comprehension — more explicit structural signals
• 1.42x Token Economics — a token/character/line composite; Calor still uses more raw tokens on small programs
• 0.98x Information Density — the single C# win

These metrics do not establish proof coverage or production defect rates. Read the results caveats alongside the numbers.

Optimizing for Agents, Not Humans

Calor deliberately optimizes for machine readability over human aesthetics:

§M{m001:Calculator}
  §F{f001:Add:pub}
    §I{i32:a}
    §I{i32:b}
    §O{i32}
    §R (+ a b)

This might look unusual to human programmers, but for an AI agent:

1. No ambiguity - Indentation defines scope and stable IDs identify blocks
2. Semantic density - Type, visibility, and ID in one declaration
3. Precise targeting - f001 uniquely identifies this function across any refactoring
4. Symbolic operations - (+ a b) is directly manipulable without parsing precedence

The Questions We're Answering

1. Can AI agents understand code better with explicit semantics?

Hypothesis: Explicit contracts, effects, and structure markers improve comprehension.

v0.12 result: 1.84x under the deterministic comprehension calculator.

2. Can AI agents find bugs more effectively with first-class contracts?

Hypothesis: Contracts surface invariant violations that would be hidden in imperative code.

v0.12 result: 1.49x under the deterministic error-detection calculator.

3. Can explicit IDs make structural targets easier to identify?

Hypothesis: Preserved explicit identifiers make structural targets less ambiguous.

v0.12 result: 1.36x under the deterministic source-pattern calculator. It does not execute agent edits, and it does not model mature C#/Roslyn refactoring tools; see the metric limits.

4. What's the cost of explicit semantics?

Honest answer: Calor pays a raw-token premium on small programs. The v0.12 token-economics composite nevertheless favors Calor at 1.42x because it also includes characters and lines. Information density narrowly favors C# at 0.98x.

Not a General-Purpose Language

Calor is not trying to replace C#, Python, or any other language. It's a research project exploring whether language design can be optimized for AI agent workflows—where the AI writes the code and humans define the outcomes.

Use Calor when:

• You want AI agents to write verifiable, contract-checked code
• You prefer defining what software should do over how it does it
• You need automatic proofs for supported contract obligations, with assumptions disclosed
• You want to shift from code review to requirements review

Use traditional languages when:

• You prefer writing code yourself
• Human readability of source is the priority
• You need ecosystem libraries without interop overhead

Frequently Asked Questions

"Do I need to learn Calor?"

You do not need to author every Calor expression by hand, but reviewers should understand the contracts, effect declarations, verification statuses, waivers, and interop boundaries they approve. An agent can translate requirements into Calor; the compiler then checks types and effects and classifies supported contract obligations.

Think of it this way: you don't need to learn assembly language to write software, and you don't need to learn Calor to benefit from it. The AI handles the language; you handle the intent.

"Do I still need to do code reviews?"

Yes. Calor changes what the review can lead with, but it does not eliminate review. Focus first on:

• Defining outcomes: What should this function guarantee? What preconditions must callers satisfy?
• Specifying contracts: The AI writes the code, but you approve the contracts (§Q preconditions, §S postconditions)
• Reviewing verification results: Which obligations are cleanly proven, and which are assumed, unknown, unsupported, unavailable, timed out, vacuous, or refuted?
• Inspecting the remainder: Generated C#, tests, interop blocks, waivers, and caller impact

Use calor review-packet to put that unproven remainder at the top of review. A proven result applies only to the specific obligation under Calor's modeled semantics; it is not a whole-program guarantee.

"What if I want to understand the code?"

Calor compiles to readable C# code. For debugging or auditing purposes, you can inspect the generated .cs files—they're standard, idiomatic C# that any .NET developer can understand. But this is the exception, not the workflow: normally you review contracts and verification results, not implementation. The Calor source is the "agent-facing" representation; the C# output exists for tooling compatibility and the rare cases when you need to investigate behavior.

"This seems verbose compared to C#"

Calor often uses more raw tokens on small examples. Its v0.12 token-economics composite favors Calor once character and line counts are included, while information density narrowly favors C#. The explicit syntax is a deliberate tradeoff, not a universal efficiency win.

"My team will never adopt this"

Adoption is gradual and low-risk:

1. Start with AI-generated modules—let your coding agent write Calor for new features
2. Review contracts first—then inspect the unproven remainder, tests, and generated boundary code
3. Interoperate seamlessly—Calor compiles to standard .NET assemblies that work with existing C# code
4. Organizational flexibility—the generated C# is always available if your organization requires it for compliance, auditing, or legacy integration

"What about tooling? IDE support?"

Calor compiles to standard .NET assemblies. That means:

• Your existing debugger works (on the generated C#)
• Your existing profiler works
• Your existing CI/CD pipeline works
• NuGet packages work

The Calor CLI includes a language server for IDE integration. VS Code extension is available for syntax highlighting and diagnostics.

"Is this production-ready?"

Calor is a pre-1.0 research project exploring AI-native language design. It emits strongly typed C# for .NET, but its verifier supports only a documented subset. Forms outside that subset report unsupported; modeled proofs that depend on named assumptions report assumed. Neither is presented as a clean proof. Conversion and tooling also retain known limitations. Start with a narrow pilot, keep generated C# and tests in review, and follow the adoption playbook and verification guarantees before expanding its role.

Learn More

• Design Principles - The five core principles behind Calor
• Stable Identifiers - How language-level IDs enable reliable AI workflows
• Tradeoffs - What Calor gives up for explicitness
• Static Contract Verification - Proving contracts at compile time with Z3
• Benchmarking - How we measure success