A gentle introduction · for the curious beginner
A normal program asks is x equal to 5? — a question with a
crisp yes or no. Kimiya is a small language for programs that must ask a different kind of
question: do these two texts mean the same thing? Those answers come from a language
model, and language models are often right, sometimes wrong, and never certain. This
is a tour of how you write programs on top of that — and still get a guarantee at the end.
§1 · the problem, in one line of code
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", "dihydrogen monoxide", "agua"…
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. You could try to list every synonym, but
meaning has no finite list. This one crack is the whole reason Kimiya exists.
§2 · from equality to tolerance
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:
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.
There is one surprising rule. This relation is not transitive. Ordinary equality says if a = b and b = c then a = c. Tolerance breaks that chain, on purpose — for the same reason many small rounding steps drift into a big error:
"the cat sat" ∼ "a cat was sitting" ∼ "a feline rested" ∼ "an animal paused"
each step is fine … but the ends no longer mean the same thing.
Allowing the chain would smuggle back exactly the drift you were trying to prevent. Keeping the relation honest — usable one step at a time, never chained for free — is the first thing that makes Kimiya safe. Reconnecting “like with like” across a step is later recovered, but at a measured price (§7).
§3 · the instrument with a spec sheet
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.
Now the model’s fallibility is not a vague worry — it is two numbers you can do arithmetic with. A judgment is no longer “trust the AI”; it is “read this instrument, whose error is 0.04.” Everything else in Kimiya is built to carry those numbers faithfully from the instrument to the final answer.
§4 · three verbs
Kimiya’s entire instruction set is three instruments, each with its own datasheet:
gen<Summary>(article)judge<5,4/5>(article entails claim) — poll 5 times, accept if 4 agree.select<0.95>(query, corpus) — guaranteed to surface ≥95% of what matters.That <5,4/5> is doing real work: asking the instrument five times and
taking a vote is how you turn a shaky judgment into a steadier one — the same reason you take a
measurement twice. (There is a limit to how much this helps, and Kimiya knows exactly what it is;
that is §7’s catch.)
§5 · control flow you can trust
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 entails claim) under k_faithful then keep(claim) else regen
And the idiom that recurs everywhere in the language — produce, then verify, and retry until verification passes — is a loop whose exit condition is a judgment, with a budget so it can never run forever:
summary := retry s := gen<Summary>(article) until judge<5,4/5> (article entails s) under k_faithful budget 4 -- try at most 4 times, then give up honestly commit(summary)
If four attempts all fail the check, the program does not push ahead on unverified output — it abstains (Kimiya writes this outcome ✠). A program that cannot meet its bar says so, out loud, rather than returning a confident wrong answer. Failure is never silent.
§6 · the reliability invoice
Here is the payoff. Because every step carries its datasheet, a finished Kimiya program comes with a certificate — a plain statement of the form:
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. Drag the sliders and watch the invoice — and notice which instrument is binding, the weakest link that caps the total:
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
The tempting shortcut is: if a judgment is shaky, 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.
Retry is sound only while the judge’s false-accept rate stays below a line set by the generator’s quality: α ≤ g·β·(1−θ) / ((1−g)·θ). Inside the line, checking genuinely helps. Outside it, a judgment that keeps saying “looks good” tells you nothing — it is measuring itself.
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
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.
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.
on the name
In classical Arabic, kīmiyā — alchemy — named the medium of transmutation, and the phrase kīmiyā al-X meant the means of obtaining X. Al-Ghazālī’s Kīmiyā-yi Saʿādat is “the alchemy of happiness.” This language is meant as a kīmiyā al-ʿaql: a means of obtaining warranted reasoning from a stochastic substrate — turning the base metal of an unreliable guess into something you can stand behind.
The homage is load-bearing. Al-Ghazālī’s deepest objection was to those who claim demonstrative certainty where the conditions for demonstration cannot be met — and that is exactly the failure a logic for machine reasoning must be engineered not to commit. So Kimiya’s guarantees are conditional, cited, and re-testable; and where the conditions fail, it is built to withhold the certificate rather than fake one. The aim was never to make a stochastic substrate look certain. It was to say precisely, and honestly, how much certainty the instruments will bear.
read on
This was the intuition. The full calculus, the proof rules, and the theorems behind every claim here — amplification, the Goodhart boundary, graded substitution, audit locality — are in the paper. Each named result is machine-checked in Coq, so the guarantees are verified, not just argued.
The proof repository goes public in September 2026.