Programming when your data is meaning how to build reliable software on an unreliable AI

§1 · the problem, in one line of code

Equality is too strict for meaning

The problem

Suppose you are grading a quiz. The model answer is "water". A student writes "H₂O". Your first instinct is the tool every programmer reaches for:

if answer == "water":  award_mark()   # ✗ fails on "H₂O", "agua", …

What went wrong

The comparison == checks whether two things are identical strings. But you did not want identical strings — you wanted the same meaning. Every correct answer phrased differently slips through the crack, and you cannot patch it by listing synonyms: meaning has no finite list.

The fixes that don’t fix it

Every programmer climbs the same ladder from here. Normalize the string — lowercase, trim — and "Water" now passes, but "H₂O" still fails. Keep a synonym list — and “the compound with formula H₂O” defeats it, because meaning has no finite list. Measure edit distance — but "water" and "waiter" are two letters apart and worlds apart, while "water" and "dihydrogen monoxide" share barely a letter. Reach for embeddings, finally: ask a model for a similarity score and accept anything above 0.8. Closest yet — and still wrong, because a score answers “how similar?” without ever asking “similar in what respect?” “Cheap flight to Tokyo” and “cheap flight from Tokyo” are nearly identical in every respect except the one that matters. Every rung fails the same way: it measures the form of the text, or an average of everything about it, when the task needed one specific slice of its meaning.

§2 · from equality to tolerance

“The same” always means “the same for a purpose”

Core idea

Kimiya replaces exact equality with a softer relation, written a ∼_κ b and read “a and b are the same, for the purpose κ.” The purpose κ is not vague hand-waving — it is a value you write down, listing what must be preserved and what may be lost:

Example

context k_answer:                 -- the purpose: grading a short answer
  domain     = "a quiz answer"
  preserve   = [meaning, key_facts]   -- these must match
  allow_loss = [wording, spelling, order]   -- these may differ

Under k_answer, "H₂O" and "water" count as the same; under a chemistry-notation purpose that preserved exact formulae, they might not. The purpose makes the question well-posed: “are these equal?” has no answer until you say equal in what respect.

The surprising part

This relation is not transitive. Ordinary equality says if a = b and b = c then a = c. Tolerance refuses that chain — and you can verify the refusal with your own eyes. Write the purpose down first:

context k_touchup:               -- matching paint for a touch-up
  domain     = "wall paint, judged by eye"
  preserve   = [appearance_to_the_eye]
  allow_loss = [batch, pigment_recipe]

chip₁ ∼ chip₂ ∼ … ∼ chip₁₄ — every adjacent pair passes. chip₁ ≁ chip₁₄.

Every adjacent pair passes k_touchup: you would happily touch up a scratch in one with the other. The two ends fail it: nobody would. Your eyes just made thirteen yes-judgments and one no-judgment, under one fixed purpose — and the chain broke anyway. (This is Poincaré’s old observation about measurement, the very example the mathematics of tolerance relations was invented for.)

Language does the same thing without colors. Along a river valley, each village understands the next village’s speech, yet the two ends of the valley cannot understand each other at all — linguists call it a dialect continuum. A paraphrase of a paraphrase of a paraphrase drifts the same way. Non-transitivity is not a quirk of the definition; it is the shape of meaning.

The objection, answered with arithmetic

A careful reader may still push back: “those judgments were perceptual — with the tolerance stated as a number, surely the chain holds?” No — and here nothing is left to the eye. Fix one purpose, write its tolerance down, and never switch it:

context k_walk:                   -- planning today's itinerary
  domain     = "walking time between stops"
  preserve   = [arrival_window]     -- to within six minutes
  allow_loss = [minute_precision]

Under k_walk, held fixed throughout: 14 min ∼ 20 min (six apart — same plan), and 20 min ∼ 26 min (six apart — same plan). But 14 min ≁ 26 min: twelve apart, and your itinerary changes. One purpose, one tolerance, no switching — and transitivity fails as plain arithmetic. Each step stayed inside the tolerance; the chain left it.

§3 · the instrument with a spec sheet

Treat the AI as a measuring instrument, not an oracle

Core idea

Who decides whether two texts mean the same? A language model. But “the AI decides” is a scary thing to build on. Kimiya reframes it: the model is an instrument, like a COVID test or a thermometer — usually right, sometimes wrong, and, crucially, shipped with a spec sheet that states exactly how wrong. Kimiya calls that spec sheet a datasheet.

Example — a judge’s datasheet

Where the numbers come from

Nobody guesses these numbers, and — crucially — the model is never asked to report them about itself. They are measured, the way any instrument is calibrated: run the judge on a few hundred cases where the right answer is independently known, and count. How often it says “yes” when it should is β; how often it says “yes” when it shouldn’t is α. If you lived through the pandemic you already know this pair by other names — a test’s sensitivity and its false-positive rate — and you already know how to think with them: a positive result from a test with a known false-positive rate is evidence, not proof, and exactly how much evidence is a calculation, not a feeling.

The third number, ρ, records something peculiar to this kind of instrument. Ask the same model the same question twice and you do not get two independent opinions — you get roughly the same opinion twice, the way asking one person twice does not convene a committee. ρ measures that “roughly,” and — counter to the instinct that consistency is good — lower is better: what repeated measurement needs is independently scattered mistakes, which a vote can cancel. A judge whose errors are correlated repeats the same mistake five times and delivers a unanimous wrong answer — confidence without information.

Because “lower is better” cuts against the grain of reading, these pages also use ρ’s positive twin: diversity = 1 − ρ — the fraction of a second opinion that is genuinely new — which points the intuitive way: higher diversity is better, just like higher β. The formal sheet records ρ (it is a true correlation coefficient, and the theorems consume it as one); diversity is the word to think with. It is also the ensemble-learning literature’s own term for exactly this property. ρ — or its diversity — is the number that decides how much re-asking actually helps (§4).

The fine print — and it is load-bearing

A thermometer calibrated for body temperature is not thereby calibrated for molten steel. A datasheet, likewise, is measured on a family of tasks — say, short grounded questions about provided text — and it holds only there. It also names the exact model version it was measured on: models drift behind stable names, so when the version changes, the instrument is re-tested, and certificates leaning on the old sheet say so. Every guarantee on this page is relative to its cited datasheets, the way a lab result is relative to the calibration of the machine that produced it.

Why it matters

Now the model’s fallibility is not a vague worry — it is three measured numbers you can do arithmetic with. A judgment is no longer “trust the AI”; it is “read this instrument, whose false-accept rate is 0.04.” Everything else in Kimiya is built to carry those numbers faithfully from the instrument all the way to the final answer.

§4 · three verbs

Produce, discriminate, find

The whole instruction set

Kimiya’s entire instruction set — everything a program can ask of the model — is three verbs. Each is an instrument in §3’s sense: it ships with a datasheet, and the number on that sheet is a different kind of promise, which is why there are three verbs and not one.

gen — produce

gen<Summary>(article)          -- “write me a Summary, working from this article”

gen asks the model to write something new: a summary, an answer, a candidate solution. The angle brackets name the schema — the shape the output must take (here, a Summary); the parentheses hold the material it works from. What comes back is a draft, and Kimiya treats every draft as untrusted. Accordingly, gen’s datasheet number is deliberately modest: how often its output is even well-formed — a valid Summary at all. Whether the draft is right is never gen’s claim to make; that question always goes to a different instrument.

judge — discriminate

context k_faithful:             -- the purpose: faithfulness to a source
  domain     = "whether a claim is supported by a given article"
  preserve   = [facts, claims, attribution]
  allow_loss = [wording, order, emphasis]

judge<5,4/5> (article |= claim) under k_faithful
                                -- “ask 5 times: does the article actually support
                                --  this claim? accept if at least 4 say yes”

judge asks one yes/no question about meaning and returns a verdict with a known error rate. The question here is entailment — the |= sign, read “entails”: does the article genuinely support the claim, or merely sit near it? The under k_faithful names the purpose the question is asked under — a context declared exactly as in §2, shown above it: its preserve list is what “support” must respect (the facts, the claims, who said what), and its allow_loss is what may differ (the phrasing). Without that declaration, “faithful” would be a vibe; with it, the judge is answering a well-posed question. The <5,4/5> is the panel: convene the instrument five times, accept only if four agree — and it is this exact configuration, panel and all, whose datasheet supplies the α and β the verdict is read at. A judge never writes anything; it only answers the question it is asked.

select — find

select<0.95>(query, corpus)      -- “find what matters for this query;
                                --  miss at most 5% of it”

select searches a pile for the items relevant to a query and returns them. Its number, recall, is a promise about what it did not return: this retrieval configuration is calibrated so that at least 95% of the genuinely relevant items are surfaced. Notice this is a different kind of promise from a judge’s. A judge promises “my verdicts are rarely wrong”; a retriever promises “I rarely missed anything” — an error rate versus a coverage floor. A perfect judge tells you nothing about what you never showed it, which is why finding is its own instrument and not a judgment in disguise.

Why exactly three

The triad is not a style choice. Each verb is the carrier of one measured quantity that the proof rules will later spend: gen carries how often its drafts are even valid, judge carries its error pair (α, β), and select carries recall — how much of what mattered it surfaced. Remove any one and some guarantee downstream loses the number it is computed from. Note too that a judge’s error and a retriever’s recall are different kinds of promise — “my verdicts are rarely wrong” versus “I rarely missed anything” — which is why they are separate instruments and not one.

One producer — and it is never trusted

gen is the only verb that creates anything, and Kimiya treats its output as untrusted, always. A draft is a draft: free to make, worth nothing until a different instrument has judged it or a mechanical check has confirmed it. This single rule — producers propose, verifiers dispose — is the spine the whole language hangs on.

How much does re-asking actually buy?

That <5,4/5> is doing real work, and it is worth seeing exactly how much. The point of a panel is steadiness: one try wobbles, and averaging tries shrinks the wobble — with truly independent tries, five votes make the verdict five times steadier than one, the standard statistical discount for measuring twice. Correlation spoils the discount, because the shared part of the errors is identical in every try, and averaging identical things changes nothing. The honest measure is the effective vote count: a panel of k tries at correlation ρ is exactly as steady as k_eff = k / (1 + ρ·(k−1)) truly independent votes. Check it at the ends: at ρ = 0 it gives k_eff = k, full value; at ρ = 1 it gives k_eff = 1 for every k — a thousand re-asks, one vote.

And the formula hides a ceiling. Let the panel grow forever and k_eff climbs toward 1/ρ — and stops. At ρ = 0.30, no panel on earth — five polls or five thousand — is ever worth more than about 3⅓ votes. (The ceiling is one of the paper’s machine-checked results.) Past a point, buying more polls buys nothing at all.

§5 · control flow you can trust

Branches and loops, driven by judgments

Core idea

In an ordinary language, if tests a boolean and while loops on one. Kimiya’s two control structures test a judgment instead:

if judge<5,4/5> (article |= claim) under k_faithful:
    keep(claim)
else:
    regen()

The recurring idiom — produce, verify, retry

The pattern that recurs everywhere in the language is produce, then verify, and retry until verification passes — a loop whose exit condition is a judgment, with a budget so it can never run forever:

summary := retry budget 4 until judge<5,4/5> (article |= summary.text) under k_faithful:
    summary := gen<Summary>(article)   -- at most 4 drafts; then give up honestly
commit(summary)

Read it as a loop, header first. The budget is declared up front — at most four rounds — and the until names the exit test: the five-vote panel judging whether the article supports the draft. The indented body is one round’s work: draft a summary. If the panel accepts, the loop ends and the accepted draft is the retry’s value, here committed; if the budget runs out first, the program abstains (✠) rather than proceeding. under k_faithful names the purpose, so “faithful to the article” has a written meaning; the budget makes the loop finite by construction, not by hope.

Two grades of truth

One more instrument belongs in this picture, and it is not an AI at all. check tests what a machine can verify mechanically — a count, a database row, an exact match, a file’s existence. A check that passes is not “probably right”; it is right, with certainty 1, and it costs no reliability. Kimiya keeps the two grades strictly apart: judged truth arrives at a measured error rate, checked truth arrives exact. And the strongest programs in the language share one architecture: judgments steer the work — which draft to keep, when to retry — while a kernel check has the final word wherever one exists. Under that discipline a judge’s mistake costs a wasted attempt, never a false answer: the lie is caught at the check before anything commits. (All three case studies run on exactly this architecture.)

The shape of a program

§6 · the reliability invoice

The program hands you a number

The payoff

Because every step carries its datasheet, a finished Kimiya program comes with a certificate — a plain statement of the form:

Read that sentence the way you would read a contract. “Provided the cited datasheets hold” is §3’s fine print made explicit: the number is relative to the instruments’ calibration, exactly as a lab report is relative to the lab’s. And the “≥” matters: the certificate is a floor, not an estimate — the program may do better; it may not claim more.

How the number is built

How is that number computed? The same way you reason about a chain: it is only as strong as its links, and the reliabilities multiply. If retrieval surfaces the right source ≥95% of the time, and the verified answer is right ≥92.8% of the time, the whole pipeline certifies at 0.95 × 0.928 = 0.881. (That 0.928 is not a guess either: it is what the retry theorem computes for a loop like §5’s, from the generator’s quality and the judge’s α and β across four attempts — every factor in the invoice traces back to a datasheet and a theorem.) Drag the sliders and watch the invoice — and notice which instrument is binding, the weakest link that caps the total:

Try the numbers

Why it matters

This is why the certificate is useful even when the model is imperfect: it never claims more than the instruments support, and it shows you exactly where to spend to do better. Wanting a higher number? The invoice tells you whether to buy a better retriever or a better judge — not to guess.

§7 · the catch you cannot cheat

You cannot reliably grade your own homework

The tempting shortcut

If a judgment is shaky, why not just check it with another judgment from the same model? Kimiya proves there is a hard limit to this — the Goodhart boundary. When the same kind of model both writes an answer and checks it, the check cannot rescue bad writing past a certain point. Beyond the boundary, self-judgment provably never certifies, no matter how many times you re-check.

The rule

Two symbols in the rule are new. g is the generator’s quality — the fraction of its drafts that are genuinely good before any checking. θ is the reliability you are trying to certify. Read the rule as: the shakier the generator and the higher your target, the cleaner the judge must be.

The intuition

Think about what a retry loop actually hands you: not a random draft, but a draft the judge accepted. So the only question that matters is — of all accepted drafts, how many were genuinely good? Good drafts arrive at rate g and pass at rate β; bad ones arrive at rate 1−g and sneak past at rate α. If the generator is weak and the judge flatters, the pool of acceptances fills up with well-disguised failures — and running the loop longer only harvests more of them. Retry collects whatever the judge lets through; it cannot make the judge honest. That is why the boundary compares α against a quantity built from g: the judge must be strict in proportion to how often it is offered junk.

Why it matters

This is not a warning in a manual; it is a theorem, and the language enforces it as a typing rule. It is the formal version of an idea everyone already trusts: a student who grades their own exam, using the same misunderstanding that produced the wrong answer, will happily mark it correct. Real verification needs genuine independence — a different instrument — and Kimiya makes you declare it (J ⋪ C: the judge is not the thing it judges).

§8 · why it matters

Machine writers, human auditors

The division of labor

Put the pieces together and a new division of labor appears. An AI agent can write a Kimiya program — it is just produce-verify-retry-find, composed. But the thing it hands back is not a black box you must trust or re-run. It is that certificate: a short invoice naming the declared purposes, the cited datasheets, and the reliability they add up to. A human can audit the invoice without redoing the work — checking the citations, not replaying the computation.

Where it shows up

That is the practical bet. The same shape shows up wherever meaning has to be computed at scale and the cost of a silent error is high:

The conditional jump once turned the human operator into a line of code and made programs objects of proof. AI systems today are at the pre-jump stage: their control flow lives in glue code and human babysitting, outside any formal object. Kimiya internalizes the operator as a calibrated judgment — and gives the result back its proof.

§9 · putting it together

Recap, and a few to try

The ideas, in one place

Try it yourself

Answers are hidden — think first, then reveal. (Nothing here claims “correct”; the honest word is always reliable.)

judge<5,4/5> (T |= H) under k_faithful

where it came from

The story behind the theorems

Kimiya did not start as a language. It started as a worry, became a small stubborn failure in a privacy tool, turned over on a walk — and ended up with a name settled on July 6th and an alchemical seal. The origin story has a page of its own.

case studies · the ideas on real problems

Three problems, three programs

Everything above stays abstract until it meets a real problem. Three case studies, each a page: one for the core language, two for the world-touching extension.