False Familiarity

I. A Model That Was Sure of the Wrong Thing

Ask a coding agent to reject a password made only of digits, in a language it has essentially never seen, and here is what one wrote, unprompted and unedited:

let after := str.strip_suffix(addr, "@").map(fn (rest :: Str) -> Str {
  rest
})

That's a reasonable line. In Rust, in JavaScript, in a dozen languages with a .map() method on that type, it's exactly right. In this language it isn't — there is no such method — and the edit was rejected. Rewritten. Rejected again. The model kept reaching for the same almost-right shape before it gave up on the method call entirely and fell back to something the language actually has.

The language is Lex, a programming language we're building around one idea: a program should be mechanically checkable for what it's allowed to do and whether it does what it claims, not just trusted to be. It has essentially no users outside this project. The agent is lex-code, built specifically to write it. Picking a language with no real training data and no community wasn't an accident — it was the cleanest way to ask a question that matters well beyond Lex: what actually happens when you point an LLM at something it has no real experience with, and what, if anything, helps.

The answer wasn't what we expected going in. It wasn't ignorance. It was confidence in the wrong thing.

II. The Usual Answer

Point an agent at a language, a library, or a codebase it hasn't seen enough of in training, and the standard answer is retrieval: index the docs, embed the examples, stuff the relevant chunks into context, and hope the model assembles the right thing from what it's just been handed. More context, better retrieval, a bigger window — the model didn't know, so tell it.

That's the right fix for one specific failure: the model genuinely has no idea something exists. It has never heard of a particular stdlib function, so it doesn't reach for it, and a paragraph of documentation in context fixes exactly that gap. We use retrieval for this constantly — lex-code's agents call a stdlib-lookup tool and a language-guide tool on practically every real task. That's not the failure behind the code above.

III. The Wrong Kind of Unfamiliar

Lex looks enough like the languages a model has seen billions of lines of — pattern matching, Option types (a value that might or might not be there), a functional core — that the model doesn't experience it as unfamiliar at all. It experiences it as almost Rust, or almost a stricter Python, and reaches for whatever the nearest language actually does.

Documentation competes with a prior. Verification contradicts it. That's the distinction worth being precise about — not that retrieval never helps here, but that it's the wrong kind of correction for this kind of mistake. A retrieved fact is evidence the model has to weigh against what it already (wrongly) believes, and has to notice applies to the specific thing it just wrote — a strong enough prior can outweigh it, or the model can simply fail to connect the two. A checker's verdict isn't evidence to weigh. It's a direct answer about the exact output just produced, pre-bound to it, with no inference step in between left to fail.

IV. What It Actually Looked Like

A cleaner case than the one above, same afternoon, same model, a boolean combinator:

-  has_min_length(password, 8) && has_digit(password)
+  has_min_length(password, 8) and has_digit(password)

Its own explanation afterward, unprompted: "It uses &&→and: Lex has no &&; the fix was to the and keyword." That sentence is the whole post in miniature. It didn't look anything up to write that fix. It already knew what and means — every language it's ever seen has some version of it. What it needed wasn't a fact about Lex. It was one bit of information: the thing you just wrote is wrong, delivered fast enough and specifically enough that a reasoning step it was already capable of could take it from there.

Both examples are real and unedited, recorded building lex-code's own landing page this week — nothing staged, nothing picked after the fact to make a point.

V. Why More Context Doesn't Fix It

You could imagine fixing the && case with retrieval — put "Lex has no &&, use and" in a doc chunk and hope it gets retrieved at the right moment. It might even work, some of the time, for that one fact. It does not scale: the number of "actually, not like the language you're thinking of" facts for any sufficiently rich type system is enormous, most of them are exactly the kind of small syntactic near-miss that's hardest to anticipate and index, and every one you add to context is competing for a budget that a fully local, quantized model does not have much of to begin with.

The type checker doesn't have that problem, because it isn't trying to anticipate the mistake. It's just answering, after the fact, exactly and only the question that matters: is this specific thing, right here, actually true. That answer is cheap to produce and impossible to argue with, which a paragraph of retrieved documentation is neither.

VI. The Division of Labor

None of this is an argument against retrieval. It's an argument about which question retrieval is allowed to answer. What exists is a lookup problem, and lookup tools are the right shape for it — lex-code reaches for one on nearly every task, asking the stdlib what's actually in it rather than guessing. Whether what you wrote is correct is not a lookup problem, and no amount of retrieval turns it into one. That question only has one honest source of truth: run the checker, run the examples, see what comes back.

Retrieval for facts, a contract for correctness. The first tells the model what's on the table. The second tells it, immediately and mechanically, whether it just lied to itself.

VII. The Model Doesn't Need to Be Smart

Every recording behind this ran against qwen3.8:27b-mlx, a quantized model small enough to run fully local on a laptop with no key and no cloud call. Not a frontier reasoning model. A modest, unremarkable, entirely offline one.

That it still works is the actual claim, not a footnote to it. If the approach only held up on the most capable model available, the interesting variable would be the model, and the honest conclusion would be "big models can do anything." What we watched instead was a small model be wrong, repeatedly, in exactly the way described above — and recover, most of the time, because recovering from "here is precisely what's false" only takes the kind of reasoning every model this size already has, not the kind only the largest ones do. The bar an agent has to clear isn't "know an unfamiliar language." It's "notice a checker said no, and try a different, still-logical answer." That is a much lower bar, and it's the one that was actually being tested.

It isn't a guarantee, and it's worth being precise about why. The same afternoon, a different task — validating an email address — put the same model into a real failure loop: the same near-miss edit, rejected, retried with slightly different whitespace, rejected again, several times over, before we cut the session rather than let it burn its step budget. Look closely at what was actually failing there, though: most of those rejections were the edit tool's own exact-match check refusing to apply a patch whose old text no longer matched the file — not a fresh type-check verdict naming what was semantically wrong each time. That's a different, and more instructive, failure than the && case: fast and cheap isn't sufficient on its own if the answer is only no. A signal that also says because of this, specifically is what actually lets a model try something different rather than the same near-miss again — which is the type checker's real advantage over a bare pass/fail, and exactly what was missing in the loop that didn't converge.

VIII. Beyond One Language

None of this is really about Lex specifically. It's about any domain where an agent's danger isn't ignorance but false pattern-matching — a new internal API shaped just closely enough like a public one everyone's seen, an internal VCS with different semantics than the git history a model has memorized by the terabyte, a config format that looks like YAML until the one place it doesn't. Wherever that's the actual risk, the fix has the same shape: don't try to out-document a wrong prior. Build the thing so being wrong is fast, cheap, and unambiguous to find out — and let reasoning the model already has do the rest.

It's also not a pattern we invented. DeepMind's AlphaProof and AlphaGeometry 2 pair a language model with Lean and a symbolic geometry engine the same way: the model proposes a candidate proof step, sometimes a wrong one, and the checker's answer is immediate and not up for debate — good enough, on real International Mathematical Olympiad problems, for silver-medal-level results, published in Nature. FunSearch runs the identical loop over code instead of proofs: an LLM proposes a program, a plain evaluator function scores it, and only what actually verifies survives to the next generation — enough to find genuinely new constructions in an open combinatorics problem no one had solved. Neither system got better by being told more about the problem. They got better by being wrong quickly, cheaply, and unambiguously, over and over, until they weren't.

Lex just happens to be the place that fix is load-bearing by design: a type checker and a declared acceptance aren't bolted on to catch mistakes after the fact, they're the whole mechanism the agent is iterating against, turn by turn. Trust by verification, not comprehension was always the claim at the level of a finished result. This is what it looks like one keystroke at a time.

IX. Where People Push Back

"You've shown two examples, one recovery and one failure loop. Isn't that just anecdote?" Yes, honestly — this is a field report, not a controlled study, and it's reported that way on purpose: the failure case is in here specifically so the piece doesn't read as two cherry-picked wins. What generalizes isn't "this model always recovers." It's the structural claim: the checker's answer is fast and unambiguous either way, which is a property of the mechanism, not a promise about any one model's reasoning depth on any one mistake.

"A compiler erroring on wrong syntax isn't a new idea — every language has had this since forever." Correct, and that's not the claim. The type checker itself is old. What's specific here is which failure it's being aimed at: not typos, not logic bugs in the ordinary sense, but a model's confident borrowing from a language it actually knows well. That's a different failure mode than the one compilers are usually praised for catching, and it's the one retrieval structurally cannot touch.

"You said lex-code calls a stdlib lookup tool constantly. Isn't retrieval doing most of the real work here after all?" It's doing real work, on a different question. Section VI is trying to say this precisely rather than gesture at it: retrieval answers what exists; it does not and cannot answer whether what you wrote is correct. Both are needed. They are not substitutes for each other, and conflating them is exactly the mistake this piece is arguing against.

"This only works because Lex has a fast, cheap, run-everywhere type checker. Most unfamiliar domains don't have anything like that." True, and worth saying plainly rather than implying otherwise. A legacy codebase's undocumented conventions, an internal API with no schema, a VCS with no equivalent of git status — none of that is mechanically checkable for free. The approach needs something that can judge correctness cheaply: a type checker, a test suite, an evaluator function, a schema. Where nothing like that exists, building or exposing it is the actual engineering work — this piece isn't claiming that work away, it's naming it as the prerequisite.

"A type checker only proves the code is well-typed, not that the logic is right — doesn't that overstate what verification buys you?" Yes, and it's a real limit, not a rounding error. lex-code's own examples {} blocks push further than a bare type check — an oracle over concrete input/output pairs, not just shapes — but even that only proves the stated examples hold, not that the implementation is correct in general; a model under pressure can satisfy a handful of examples by special-casing them. What this piece is claiming is narrower than "verification proves correctness." It's "verification answers is this specific thing false precisely and cheaply" — a smaller claim, and the one the evidence here actually supports.

— Alfonso Sastre, September 24, 2026