AI wrote my compiler. A mathematical proof checks its work on every build.
DEV Community

AI wrote my compiler. A mathematical proof checks its work on every build.

The Metric That Everything Answers To

Four months ago I published a claim with weak evidence behind it: that how easy a language is for an AI to write correctly depends on the language's design, not on which model you throw at it. The evidence at the time was one toy language that passed all 8 of my test problems - but took 3x longer than Ruby to get there.

My working theory was that the gap was just a training-data problem. Put more of this language's code on the internet, and the model would eventually catch up on its own. That didn't happen. There's barely more Almide code on the public internet today than there was four months ago. And Claude's current models now solve all 20 of my test problems on the first or second try - faster, and in fewer lines, than mature languages with a decade of training data behind them.

Here's what actually changed instead.

Almide is a language designed to be written by AI agents, and for the last 4.5 months I've barely touched its compiler's source myself. The commit log's Co-Authored-By: Claude trailers tell that story better than I can. Steering a fleet of stateless agents through a codebase this size needed a policy that survives the fact that none of them remember the last session.

The fix was mundane: a file every agent reads before it does anything. Line one of CLAUDE.md:

Every design decision serves one metric: modification survival rate.

Modification Survival Rate (MSR) is not "did the model get it right on the first try." It's: let the model write code, compile it, and if compilation fails, hand it the raw error message and let it retry - up to 3 times. What gets measured is whether the loop converges on working code, not whether the first draft was perfect.

Model writes code โ†’ compile succeeds โ†’ pass fails โ†’ show raw compiler error โ†’ model retries โ†’ compile again
(after 3 failed retries โ†’ fail)

That framing - score the retry loop, not the first draft - turned out to be the single highest-leverage decision in this project. It means every syntax choice, every error message, every stdlib function name gets judged by one question: does this help the model recover from being wrong, not just avoid being wrong in the first place.

Cutting Syntax Down to What Has Evidence Behind It

Once MSR was the metric, syntax debates stopped being taste and became measurable. The first one: should a lambda be written fn(x) => x + 1 or (x) => x + 1? Two characters, and I was sure the shorter one would be easier for a model to get right.

Asking a model which it prefers is useless - models are sycophantic by default and will validate whichever option you hint you like. So I built grammar-lab: the same code-fixing task, run against both syntaxes, scored by whether the output compiles and passes.

https://github.com/almide/almide/tree/develop/research/grammar-lab/

Model fn-lambda paren-lambda p-value
claude-sonnet-4-6 100% (25/25) 100% (25/25) 1.0
claude-haiku-4-5 86% (26/30) 86% (26/30) 1.0

Sonnet hits a ceiling on both - no signal there. Haiku, the weaker model, is where a real difference would show up if one existed. It didn't: identical pass rates, p=1.0, the flattest possible null result. No evidence of a difference means the extra fn characters were pure noise, so I cut them.

Frontier models essentially never get syntax wrong on a language they've never seen before - that's not where the failures live.

Where Do the Failures Actually Live?

There's a clean way to find out, borrowed from someone else's evaluation of a different AI-targeted language: hand a model one cheatsheet, zero other context, and have it implement something nobody writes casually - a red-black tree - from scratch. I ran the same setup on Almide: Claude Opus, one CHEATSHEET.md file, two problems (a basic calculator and red-black tree insert/delete), five independent runs each, scored by a separate judge model blind to any target answer.

All 10 runs eventually finished. Only 2 of the 10 finished clean on the first try. The other 8 all failed at least once - and the failure category was almost perfectly one-sided:

  • Syntax errors: 0
  • Semantic errors: 0
  • Stdlib hallucinations: 9 of 9 first failures

Frontier models essentially never get a new language's grammar wrong. What they get wrong is guessing at a library they've never seen. io.read_line doesn't return a Result, but the model assumed it did and slapped a ! unwrap on it. int.parse is the real function; the model invented int.from_string because that's what half a dozen other languages call it. Plugging the actual gap was almost insultingly simple - 13 lines added to the cheatsheet under "stdin & parsing" and that class of failure stopped.

The second failure mode was different: habits imported wholesale from other languages. OCaml's let ... in and while ... do, !x for boolean negation, an invented .to_upper() method that doesn't exist. This isn't about not knowing Almide's grammar. It's a model averaging across every language it's ever seen and defaulting to the blend. A dedicated detector catches these and returns a diagnostic that says, plainly, "Almide writes this as ___."

Three failure categories, in order of how they get fixed:

  1. Stdlib guesses โ†’ fixed by writing the real signature down once
  2. Cross-language habits โ†’ fixed by a detector plus a diagnostic
  3. And the one that took the longest to find: the compiler's own advice lying to the model

Error Messages as an API, Not a Paragraph for a Human

In most languages, a compile error is prose aimed at a person. In Almide, the thing reading that error is the same model that wrote the code and is about to write the fix, with no human in the loop. That reframes the error message completely: not documentation, but an API response, and like any API response it can be wrong in ways that actively mislead the caller.

One real case: a model wrote let (value, symbol) = pair - value was meant as a throwaway local name. Almide also ships a stdlib module literally named value. The type checker at the time mishandled this destructuring pattern and misdiagnosed value as undefined, then suggested:

error: undefined variable 'value'
hint: Add `import value` โ† wrong

The model dutifully added the import and dug itself in deeper. The error didn't just fail to help; it actively lied, and the model trusted it. The fix was to exclude common local-variable names like value and error from the import-suggestion heuristic. Diagnostics that actively steer a model into a worse state go on a running list and get closed out one at a time.

The reference point here is Elm, well known for treating compiler errors as a conversation rather than a verdict: https://elm-lang.org/news/compiler-errors-for-humans. Almide pushes that a step further by swapping the other side of the conversation from a human to a model.

A current diagnostic looks like this:

error[E001]: type mismatch in fn 'sum_digits': expected Int but got Unit
 --> unit_leak.almd:2:25
 in fn 'sum_digits' here:
   let abs_n = int.abs(n)
 hint: Fix the expression type or change the expected type
 try:
   // fn body ends with `let abs_n = ...` (a statement, returns Unit).
   // Add `abs_n` as the trailing expression so the fn returns Int:
   //
   //   let abs_n = <computation>
   //   abs_n               // <-- add this line

error[E001] is one of 31 error codes, each shipped with its own docs and a repro test. CI rejects a new diagnostic code that lacks either. try: is not a filled-in template; it's a paste-able fix specific to that exact failure. "Type mismatch" is a verdict; "add abs_n on the next line" is an instruction a model can execute without reasoning about it further, and that's the part that actually moves the retry loop forward.

The docs behind each code aren't hosted anywhere external: almide explain E010 returns the full writeup (common causes, a real diagnostic sample, fix options) straight from the compiler binary. Two reasons for that: a language this new has no Stack Overflow answers to fall back on, and the docs can never drift out of sync with the compiler that's running, because they ship in the same binary.

The next question follows naturally: if try: is literally paste-able code, why is a model pasting it at all? almide fix app.almd applies deterministic fixes directly, for the four categories that have exactly one correct rewrite regardless of context:

  • Missing imports (json, fs, etc.): added automatically
  • Hallucinated comparison functions (int.gt(n, 0)): rewritten to the real operator (n > 0)
  • Stray OCaml let ... in: the trailing in is stripped
  • Redundant return: removed, since Almide uses trailing-expression returns

almide fix --json emits a machine-readable report, meant to be consumed by an agent's own retry loop rather than read by a person:

Compile fails โ†’ almide fix applies deterministic rewrites โ†’ recheck
clean โ†’ no model needed
errors remain โ†’ only judgment-requiring fixes reach the model

Every deterministic fix almide fix applies is one fewer round trip through a model, one fewer chance to introduce a new mistake while fixing the old one.

Measuring the Effect Daily, on Purpose-Picked Weak Models

Fixing a diagnostic and feeling like it helped are different things. Almide Dojo is the daily instrument that closes that gap:

https://github.com/almide/almide-dojo

  • 31 problems, fizzbuzz through red-black tree, ranked by difficulty
  • A GitHub Actions job runs all 31 daily against two models
  • Compile failures get up to 3 retries with the raw diagnostic shown
  • Results land in a dated commit every day

The models are deliberately not Claude. Dojo runs two Llama models via Cloudflare Workers AI: 3.3 70B and a considerably smaller 3.1 8B. Cost is half the reason. The other half: instrument sensitivity. Claude scored 29/30 the day Dojo launched, and a model pinned at the ceiling can't show you whether a fix moved anything. The same logic that put Haiku in grammar-lab put Llama in Dojo. Running both sizes side by side surfaces something a single model wouldn't:

  • 70B: 16/31 correct on the first try, climbing to 22/31 once retries are allowed.
  • 8B: stuck at 10/31 on the first try - and stays there. 21 failed problems ร— 3 retries = 63 additional attempts, and not one of them converges.

The gap between those two numbers is exactly "can this model read an error and move toward the fix," isolated from everything else. That's why the dashboard's headline metric isn't first-try accuracy: it's the percentage solved within 3 tries. First-try accuracy measures the model. This measures the compiler's side of the conversation.

The dashboard's other load-bearing number is a ranking of which diagnostic codes still block a model after all 3 retries are burned. That ranking is the backlog - it says, directly, which parts of the compiler still need work, ranked by how often they defeat the retry loop.

Daily 12:00 UTC: models solve 31 problems โ†’ failures logged โ†’ turned into diagnostic / stdlib fix candidates โ†’ compiler patched โ†’ (next day) models solve 31 problems again

Neither Llama model has changed in months. The pass rate has. That's the whole point of running it daily against static models - any movement in the numbers is attributable to the language, not the AI.

Deleting Syntax is the Hardest Call, and the Right One

Almide v0.1.0 used a single keyword, do, for two unrelated jobs: wrapping loop bodies and wrapping effect-fn bodies. One keyword, two meanings - exactly the kind of ambiguity that makes a model hesitate mid-generation and produces inconsistent output. I wrote the removal plan one afternoon and rewrote all 66 do blocks in the repo to while / guard that same night. I considered a deprecation period with warnings first. I didn't do it - a language that hasn't hit 1.0 doesn't owe anyone a migration window, and every day do stays half-valid is another day a model can generate it.

Write do in Almide today and the compiler returns exactly one line:

`do` blocks have been removed - use `while` for loops or remove `do` from effect fn bodies

No fallback, no soft warning. Just a sign pointing at what to write instead.

What Was Actually Being Optimized For

Stack these up and the conclusion is uncomfortable at first: trying to make a model never make a mistake is the wrong target. Model output is sampled from a distribution, and some rate of mistakes is a property of how the thing works, not a bug to be patched away.

What's actually achievable is three things, and none of them are about making the model smarter:

  1. Cut the number of ways to write the same thing. Every syntax choice removed is one fewer place a model can hesitate and diverge. Deleting do wasn't cleanup; it was this principle applied directly.
  2. Force every remaining mistake to fail loudly. The dangerous failure doesn't look like a compile error. It looks like code that runs and returns a subtly wrong answer without complaint. Every design choice here is aimed at converting silent wrong-answers into diagnostics that stop the build.
  3. Pave the road back from a loud failure to correct code. hint, try, almide explain, almide fix: with all four in place, the 3-retry loop from MSR usually finds its way home. In practice, that's close enough to first-try correctness to matter just as much.

The name of the metric was the answer the whole time. Modification Survival Rate doesn't ask whether the first draft was right. It asks whether the loop, wrong, then corrected, then right, closes. Every decision in this section was aimed at making that loop shorter and more reliable, not at making the first draft perfect.

Running a Fleet of Agents That Don't Remember Each Other

None of this works without a way to run many agents against one codebase without it collapsing into chaos. The starting constraint is structural, not motivational: an agent's memory resets completely between sessions. The next one called doesn't know the last one existed, let alone what it learned. Policy can't live in a conversation - it has to live in a file that gets re-read every single time. That's what CLAUDE.md actually is. Every

Comments

No comments yet. Start the discussion.