v0.22.0—Bounded nullability checks and practical .NET migration guidance.See what's new

Calor logoCalor
DocsGetting StartedBenchmarksChangelog
Documentation

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:

QuestionTraditional LanguagesCalor
What does this function do?Infer from implementationExplicit contracts (§Q, §S)
What are the side effects?Guess from I/O patternsDeclared with §E{cw,fs:r,net:rw}
What constraints must hold?Parse exception patternsFirst-class preconditions/postconditions
How do I precisely reference this?Hope line numbers don't changeOptional stable IDs (§F{f001:Main})
Where does this scope end?Count braces, handle nestingIndentation (Python-style)

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.

Constrained C#Calor
Compiles successfullyCompiles + contracts classified
Syntactically validSupported obligations can be proven
Hidden invariant violationsCounterexamples when the model can refute them
Implicit side effectsDeclared and enforced

What Constrained Decoding Can't Catch

C#
// LLGuidance-constrained C# — syntactically perfect, semantically buggy
public int Divide(int a, int b) {
    return a / b;  // Compiles fine. Crashes on b=0.
}
Calor
// 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 static benchmark prepared for publication with v0.22.0 was recorded on 2026-09-15 for 30 repetitions from source c2a8816d, which still declared compiler v0.21.0 before the release version bump. It 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.97x Information Density — the single C# win

Source pairs are not all behaviorally equivalent, and the deterministic repetitions are not independent samples. These metrics do not establish a measured language, agent-productivity, correctness, or safety advantage, 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:

Calor
§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.

Calculator score: 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.

Calculator score: 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.

Calculator score: 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 token-economics composite nevertheless favors Calor at 1.42x because it also includes characters and lines. Information density narrowly favors C# at 0.97x.

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.

For you if / Not for you if

For you if…Not for you if…
You ship .NET code with AI coding agents and want compile-time effect checks, runtime contracts, and explicit proof verdictsYour team dislikes explicit annotations or prefers to author every line of source by hand
You are comfortable running a pre-1.0 tool from a single maintainerYou need a stable v1 API today or commercial support
You want to test whether review can lead with requirements, contracts, and proof verdicts on your workloadHuman readability of source is the priority and no agent is involved
You value a tested eject path — the generated C# is yours and can be built without CalorYou depend on features that would require heavy interop (delegate-heavy or reflection-heavy service layers)

See the adoption playbook for the incremental path and the verification guarantees for what proven — and every other verdict — actually promises.

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.

An agent can author Calor, but reviewers still need enough language knowledge to understand the specifications and boundaries they approve. The agent does not remove human ownership of intent, tests, or accepted behavior.

"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 emits ordinary C# that can be inspected with .NET tooling. Generated code is a compatibility and exit artifact, not proof that every lowering is idiomatic or correct. Review contracts and verification results first, then inspect generated C#, tests, interop blocks, and waivers where the evidence requires it.

"This seems verbose compared to C#"

Calor often uses more raw tokens on small examples. Its 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 can be gradual and reversible, but the project has not measured its organizational risk or total cost:

  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. Test interoperation—Calor emits .NET assemblies, but manifests, preserved C#, and unsupported forms still need review
  4. Keep the exit path tested—retain generated C# and its dependencies for compliance, auditing, or migration back to C#

"What about tooling? IDE support?"

Calor emits standard .NET assemblies and C#, so existing debuggers, profilers, CI systems, and NuGet workflows can be integrated. Verify each toolchain on your target runtime and keep generated-code/source-map limitations visible.

The Calor CLI includes a language server (calor lsp) that speaks standard LSP over stdio and works with any LSP-capable editor. The dedicated VS Code Marketplace extension was withdrawn after v0.13.1; see the changelog.

"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. No qualifying adopter, independent adopter handoff, economic advantage, or safety advantage has been established. Start with a narrow pilot, keep generated C# and tests in review, and follow the adoption playbook, verification guarantees, and research evidence status before expanding its role.

Learn More