Someone Built a Language With No Variable Names — For AI to Write

# Someone Built a Language With No Variable Names — For AI to Write

There's a new programming language on GitHub called Vera, and it makes a claim that's either brilliant or completely unhinged: programming languages should be designed for the entity that actually writes the code. And increasingly, that entity is an LLM.

The creator, Alasdair Allan (aallan on GitHub), has built something genuinely unusual. Vera has no variable names. None. Instead of let user_count = 0, you write @Int.0. The @Int is the type, and .0 means "the most recent Int binding." .1 is the one before that. This is called a typed De Bruijn index, and the argument is that LLMs are demonstrably bad at names — they choose misleading ones, reuse them wrong, and lose track of which name refers to what value across a long generation. So: remove the variable.

The HN thread from today is currently at 36 points and 18 comments, and the reactions are everything you'd expect. One camp says this is a fundamental misunderstanding of how LLMs actually succeed at coding. The other says it's the first honest attempt to design a language for the post-human-programmer reality. Both have a point.

Contracts Are Not Optional

The naming thing gets attention, but the real innovation is Vera's contract system. Every single function requires three clauses:

public fn safe_divide(@Int, @Int -> @Int)
  requires(@Int.1 != 0)
  ensures(@Int.result == @Int.0 / @Int.1)
  effects(pure)
{
  @Int.0 / @Int.1
}

requires is a precondition. ensures is a postcondition that Z3 (the SMT solver) proves statically. effects tells you what side effects the function has — and Vera is pure by default. A function that calls an LLM must declare effects(<Inference>). A function that makes HTTP requests declares effects(<Http>). If you try to call an inference function from a pure context, the compiler rejects it.

This is the part that actually makes sense for AI-generated code. The model doesn't need to be correct — it needs to be checkable. The compiler does the verification. Three-tier system: Z3 proves what it can (Tier 1), guided checks for what it can't (Tier 2), and runtime assertions as a last resort (Tier 3).

Errors Written for the Machine That Broke It

Traditional compiler errors are written for humans: expected token '{'. Vera's errors are instructions for the model that wrote the code. Each one includes what went wrong, why, how to fix it with a concrete code example, and a spec reference. There are 700+ stable error codes available as structured JSON. The idea is that an agent gets a compiler error, feeds it back to the model, and the model gets an actual instruction — not just a line number and a cryptic message.

The Benchmark

Allan also published VeraBench, a 50-problem benchmark across 5 difficulty tiers with 6 models. The headline number: Kimi K2.5 gets 100% run_correct on Vera, compared to 86% on Python and 91% on TypeScript. That's a real result.

But then GPT-4.1 gets 91% on Vera vs 96% on Python. Claude Opus 4: 88% vs 96%. The flagship tier averages 93% on both Vera and Python — essentially parity. So the language doesn't make things worse for most models, and it makes things dramatically better for at least one.

The caveat is that these are single-run results with high variance, and the benchmark is 50 problems written by the language's creator. Take it with a grain of salt the size of a small boulder.

The Real Question

Here's what the HN thread actually gets right in both directions. The skeptics say: LLMs are trained on billions of lines of Python, JavaScript, and Go. They have zero training data in Vera. You're asking them to write in a language they've never seen, guided only by a SKILL.md file you include in the prompt. That's fighting uphill.

The believers say: the compilation step is the safety net. The model writes Vera, the compiler verifies it, the model fixes what fails. Loop until it compiles. The language is designed for this feedback loop — every error is actionable, every contract is checkable.

Both are right. But here's the thing: we're going to see a lot more of this. Programming languages have always co-evolved with their authors. Assembly came from hardware constraints. C came from operating systems. Python came from programmer productivity. If LLMs become the dominant authors of code, the languages will adapt. Vera might not be the winner, but it's sketching the shape of something inevitable.

The feature I actually want from my copilot today isn't a new language — it's Vera's contract system bolted onto the languages I already use. Give me requires and ensures and effects on my TypeScript functions, verify them at compile time, and suddenly my AI-generated PRs have guardrails that don't depend on me catching everything in code review.

Vera is at v0.0.127 with 810+ commits, 127 releases, 3,638 tests, and 96% code coverage. It compiles to WebAssembly and runs in the browser or at the command line. It's real, it's weird, and it's worth watching.

Vera on GitHub · VeraBench · HN Discussion