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:
| Question | Traditional Languages | Calor |
|---|---|---|
| What does this function do? | Infer from implementation | Explicit contracts (§Q, §S) |
| What are the side effects? | Guess from I/O patterns | Declared with §E{cw,fs:r,net:rw} |
| What constraints must hold? | Parse exception patterns | First-class preconditions/postconditions |
| How do I precisely reference this? | Hope line numbers don't change | Unique IDs (§F{f001:Main}) |
| Where does this scope end? | Count braces, handle nesting | Matched closing tags (§/F{f001}) |
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 successfully | Compiles + contracts verified |
| Syntactically valid | Semantically proven |
| Hidden invariant violations | Caught at compile time |
| Implicit side effects | Declared and enforced |
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}(a: i32, b: i32) -> i32
§Q (!= b 0) // ← Contract: b must not be zero
§S (>= result 0) // ← Contract: result non-negative
(/ a b)
§/F{}Calor's Z3 integration proves contracts hold, or flags violations with counterexamples. No amount of grammar-constrained generation gives you this for free.
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 benchmarks show this: Calor's advantage isn't token efficiency (C# wins there). It's:
- 1.22x Error Detection — Contracts catch bugs C# misses
- 1.51x Comprehension — Explicit semantics aid understanding
- 100% Contract Verification — Z3 proves correctness statically
- 100% Effect Soundness — No hidden side effects
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)
§/F{f001}
§/M{m001}This might look unusual to human programmers, but for an AI agent:
- No ambiguity - Every scope has explicit open and close tags
- Semantic density - Type, visibility, and ID in one declaration
- Precise targeting -
f001uniquely identifies this function across any refactoring - 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.
Result: 1.46x improvement in comprehension benchmarks.
2. Can AI agents find bugs more effectively with first-class contracts?
Hypothesis: Contracts surface invariant violations that would be hidden in imperative code.
Result: 1.45x improvement in error detection benchmarks.
3. Can AI agents make more precise edits with unique IDs?
Hypothesis: Unique identifiers enable targeted modifications without collateral changes.
Result: 1.36x improvement in edit precision benchmarks.
4. What's the cost of explicit semantics?
Honest answer: Token efficiency. Calor uses more tokens than C# (0.63x ratio), trading brevity for explicitness.
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 mathematical guarantees about program behavior
- 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?"
No. You don't write Calor—your AI coding agent does. Calor is designed for AI agents to read and write, not humans. Your role shifts from writing code to defining outcomes: what should the software accomplish, what constraints must it satisfy, what behaviors are acceptable. The AI agent translates your requirements into Calor, and the compiler verifies the contracts are satisfied.
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?"
No. Instead of reviewing implementation details line-by-line, you focus 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 (
§Qpreconditions,§Spostconditions) - Reviewing verification results: Did Z3 prove the contracts? Are there counterexamples?
The compiler and verifier do the tedious work of checking implementation correctness. Your job is ensuring the requirements are correct. If the contracts pass verification, the implementation is mathematically guaranteed to satisfy them.
"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#"
Yes, Calor uses more tokens than equivalent C#. But you're not the one writing it—the AI is. The verbosity serves the AI: every extra character carries semantic meaning that helps the agent understand and modify code correctly. The Lisp-style expressions are directly manipulable without parsing precedence rules.
"My team will never adopt this"
Adoption is gradual and low-risk:
- Start with AI-generated modules—let your coding agent write Calor for new features
- Review contracts, not code—approve what the software should do, not how it does it
- Interoperate seamlessly—Calor compiles to standard .NET assemblies that work with existing C# code
- 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 research project exploring AI-native language design. The compiler produces correct, strongly-typed C# code with Z3-verified contracts. There are no experimental runtime features—just standard .NET. Whether it's "production-ready" depends on your risk tolerance and use case. We recommend starting with AI-generated modules for new features and expanding as you gain confidence in the workflow.
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