The hard part of AI-written code isn't writing it. It's trusting it.
"Looks correct" is exactly what review and tests miss — a leaked secret, an out-of-order call, a broken promise all pass inspection, then fail in production.
Heat moves that check into the compiler. Each becomes a build error, proven at compile time — not an incident found later.
Cheaper than a test, a review comment, or an outage. Proven, not guessed.
Where it pays off: the code where being wrong is expensive.
agent and LLM tool pipelines
regulated data (PCI / PHI / PII)
security-sensitive integrations
money movement and hard invariants
Not a general-purpose, rewrite-everything language. For a throwaway script the guarantees aren't worth the rigor, and Heat won't pretend otherwise.
Why now: the moment AI authors at scale is exactly when machine-checkable boundaries start paying for themselves. The proofs below are SMT-backed and runnable, not a linter's guesswork.
Heat · live demos
Watch the compiler refuse, repair, and run.
38 runnable flows — each is real heatc output captured from the
examples in this repo. Click any card to watch the broken input get refused (or healed),
then the fixed version pass.
Every demo maps to a file you can run yourself:
heatc check examples/demos/demo_<name>.heat ·
heatc check examples/basics/<name>.heat ·
heatc test examples/browser/e2e_login_test.heat.
These are packaged demo flows for learning Heat from compiler output.
Proved & protocol-checked · the AI-author frontier
Your tests pass right up until the input that breaks them shows up.
Correctness the safety lattice never touched: an SMT prover refuses code that violates its own require/ensure, the compiler refuses out-of-order actor messages, and it hands the author the real API instead of a hallucinated one.
Refused at compile time
Secret exfiltration is treated as a review problem. It should be a build error.
Unsafe agent and dependency flows are stopped before release; the fixed version then passes clean.
Refuse, then repair · heatc heal
Most compilers reject your code and leave the fix to you. Heat's compiler computes it.
These aren't model patches: the compiler derives each fix from your types and effects — deterministic, the same result every time — for a missing label, a missing IO declaration, a typo, or a missing helper body. An LLM fallback (last card) is an optional layer for the rare gap the rules can't close.
Build & run
Not a proof-of-concept — real programs handling real failure.
Everyday program shapes: bad input, malformed JSON, failed contracts, concurrent updates, and subprocess failure.
Canonical basics
The ordinary 90% of a language — the parts that aren't about refusal.
Small examples that show how ordinary programs read, validate, test, model data, and handle boundaries.
Browser automation & Playwright at scale
Refusal isn't a toy-language tax — it holds up under real workloads.
Real browser-test chores: logins, assertions, nested targets, and page text that cannot flow into unsafe sinks.
Heat