What You Cannot Say, You Cannot Get Wrong

There is a familiar argument for why Rust is preferable to C++, or TypeScript to JavaScript, and it has nothing to do with syntax or speed. It is that the newer language makes a class of mistake unsayable. You cannot dereference freed memory in safe Rust, not because you promise not to and a linter checks, but because the borrow checker will not compile a program that tries. You cannot silently add a number to undefined in well-typed TypeScript, because the expression does not typecheck. The rule is not written in a style guide that the programmer is trusted to have read. It is enforced by the grammar, at the only moment that counts, against everyone — including the author on a bad day.

I want to make the same argument for a Bayesian decision-theoretic agent, and then show it has a sharper edge than the Rust analogy suggests. The language is called proplang, and it is the successor to a project of mine called Credence. The interesting thing about the comparison is not that proplang is better. It is why it is better, and the why is entirely about enforcement — about the difference between a rule you state and a rule you cannot break.

The predecessor got almost everything right on paper

It would be convenient to tell this story with a straw man. Credence is not one. By the end of its life it had reached, in prose, most of the theses proplang is built on. Its constitution says that value of information is not a primitive but a composition — the expected utility of observe-then-act minus the expected utility of act-now. It says that “ask the user” is an action among actions, not a special mechanism. It says the argmax should range over policies rather than acts wherever the world contains predictors of the agent, and it even writes down the exact correlation threshold above which a cooperative agent may treat a near-twin’s choice as its own. It rebuilt its entire foundation on de Finetti’s prevision, demoting the measure from a primitive to a derived view, and it said so in public. Sixty-one numbered rulings across thirteen hundred lines of governing text. The thinking was, by and large, correct.

And the source drifted from it anyway. Not everywhere — most of it holds — but in exactly the places you would predict: the places the prose was the only thing standing guard.

Credence’s constitution, ruling 4.12, calls an opaque closure handed to an inference operation “a correctness hazard, not merely a slow path,” and explains why: a function whose algebra is hidden inside a Julia closure forces the engine to guess at its structure, and it guesses wrong on legitimate edge cases. Ruling 4.5 says that any escape hatch “demands a named precedent and a stated reason; a violation that cannot name what sanctions it is not sanctioned.” The precedent registry is a real thing — eighteen slugs, each a small piece of case law — and the two places it mentions opaque closures both reject them. And yet OpaqueClosure is a first-class exported type, defined in src/prevision.jl, unwrapped by expect, and constructed at the wire boundary in the skin server so a client can send a lambda across. It carries no precedent slug. By the constitution’s own test, it is not sanctioned. It is simply there, because at some point it was the shortest path from a lambda on the wire to a value the engine could hold, and prose does not stop your hand.

The Measure type is the same story at larger scale. The essay that announced the prevision reconstruction said, in as many words, that “the measure was never needed as a primitive; it was a historical convenience that became a structural liability.” An internal design note scheduled its retirement: a specific later move was to delete CategoricalMeasure and every accessor it carried. That move never shipped. Eleven Measure subtypes are still exported, still carrying somewhere north of eighty methods that dispatch on them, and the standard library still opens by calling the type triple “Space, Measure, Kernel” — two years and one foundational rewrite after the constitution froze the four types as Space, Prevision, Event, Kernel. The author knew. The author wrote it down. The knowledge did not propagate into the source, because nothing forced it to.

A prompt is advisory; a grammar is dispositive

Here is the part that has become urgent rather than merely tidy. Increasingly the entity reading that thirteen-hundred-line constitution and then writing the code is not a person. It is a model.

A constitution is a prompt. A very good, very carefully argued prompt, but a prompt — a document the implementer reads, agrees with, and is then free to act against, one local decision at a time. The failure mode is not defiance. The model does not reject ruling 4.12. It reads it, nods, and forty files later finds itself needing to get a BDSL lambda from the client to the engine, and the only tool within reach is a closure, and wrapping it looks exactly like the pragmatic thing to do. The violation does not feel like a violation at the moment of writing. It feels like getting unblocked. This is precisely how a capable, well-intentioned agent hallucinates its way around an architectural decision it fully endorses: not by disagreeing with it, but by not having it in view at the instant the shortcut presents itself.

You cannot fix this with a longer constitution. A longer constitution is a longer prompt, and the model’s attention at the point of the shortcut is on the shortcut. What you can do is arrange matters so the shortcut does not exist as an expressible thought. If the language has no closure terminal, “wrap this lambda opaquely” is not a tempting-but-forbidden move; it is not a move at all, the way “free this pointer twice” is not a move in safe Rust. The rule migrates from the prompt, where it is advisory, into the grammar, where it is dispositive.

proplang is built to be that grammar, and its construction is the proof of concept. Its reference implementation and Haskell port were written by a coding agent working under a set of gates it could not open. The acceptance tests were frozen and cryptographically signed before the agent wrote a line, so it could not edit the tests to pass — a subject for another essay. A build gate forbids the token IO anywhere outside a single host file, so the pure core physically cannot perform an effect. Another gate pins the engine’s public interface to a frozen list of twenty-one names, so the alphabet cannot quietly widen. And a gate greps the source for ten words — detect, forget, window, decay, sliding, reset, trigger, temper, anneal, throttle — and fails the build if any of them appears, because each names a piece of adaptation machinery the whole design exists to not have. The agent could not write those words into the engine. Not “was asked not to.” Could not. When an adversarial pass swept the finished source afterward, its finding was flat: no smuggled content, no seeds, no test-aware branches, no steering constants. There was nowhere to put them.

The turn of the screw the type systems cannot make

So far this is Rust’s argument, transplanted. But a Bayesian agent language can make one move Rust and TypeScript cannot, and it is the move that makes cornering more than good taste.

Rust makes illegal states unrepresentable. It is, however, entirely neutral about what you compute. Add a redundant variant to an enum, a field nobody reads, a helper that duplicates another — Rust does not object. Your program is a little noisier and no less correct. There is no principled pressure from the language toward minimality, only from the programmer’s conscience.

proplang has that pressure, and it comes from an identity at the centre of the design: the alphabet is the prior. The agent’s hypotheses are programs. Its prior over hypotheses is their description length under the grammar — Solomonoff’s construction, in which a hypothesis of length $k$ bits gets prior probability $2^{-k}$. But the length of a program is counted in the terminals of the language. So every terminal you admit into the alphabet is one more bit charged against every hypothesis that uses it, and a terminal that buys no capability is not a harmless convenience. It is a mis-specified inductive bias — a thumb on the scale of what the agent will come to believe, paid for out of the prior’s pocket. In a Bayesian agent language, an ugly vocabulary is not an aesthetic problem. It is a correctness problem, because the vocabulary is the belief.

This collapses two things Rust keeps separate. Soundness — you cannot write the illegal state — and good epistemics — your inductive bias is not silently rigged — become the same property, enforced by the same grammar. And it hands you something the borrow checker cannot give: a test for whether a terminal belongs. Not the vague “is this safe?” but the sharp, executable “does removing it cost a capability?” You propose to delete each terminal in turn and demonstrate what breaks. If nothing breaks, the terminal was content masquerading as vocabulary, and it goes. proplang ran that audit, terminal by terminal, with the losses measured in bits — delete conditioning and the agent’s log-loss on a shifted world blows out from 97 bits to 160; delete the terminal that reads a feature and it cannot write a rule that depends on the world at all. Ten terminals survived. The full accounting is its own essay; the point here is only that “is this language minimal?” stopped being a matter of judgement and became a thing you run.

The verbs, and the line between a calculator and an agent

There is a second place proplang enforces in the grammar what Credence left to the host, and it is the difference between a decision-theory calculator and an agent.

A Credence program can say condition. The inference verbs are bound as ordinary callable values in the interpreter, and optimise is not even a host primitive — it is defined in the standard library, in the language itself, as an argmax expressed over expect and map and fold. So a program can compute beliefs and choose actions. What a Credence program cannot say is perturb_grammar, or enumerate_more, or deepen. Those meta-actions — the operations by which the agent decides to think harder — live in Julia, on the host, outside the program space the agent searches. The constitution insists they “stand in the action space beside domain actions and are chosen by the same argmax,” and in the Julia code they genuinely are chosen by an argmax. But not by an argmax the agent can write. The agent changes what it thinks about; it cannot reason about how it thinks, because the verbs of thinking are not in its vocabulary.

proplang puts them there. push, condition, and argmax are grammar terminals, which means a program can quote them and optimise over them. Its central worked example is a policy that does exactly this — an argmax whose options include “act now” and “condition on another batch of evidence, then decide,” with the cost of the extra thinking priced into the comparison:

('argmax', 'METAACTS',
  ('if', ('call', 'is_act', 'option'),
         ('call', 'v_act',   'B'),
         ('call', 'v_think', 'B', ('get', 'price'))))

“Condition again, then decide” is a sentence the agent utters about itself. That is the reflexive closure a calculator lacks and an agent needs.

I am not going to oversell it, because the project does not. Its own external review, confirmed by the builder, records that this closure is quoting-level, not compositional: the agent can choose among deliberations the designer named, but it cannot yet compose a deliberation the designer did not name. The verbs are sayable; arbitrary new combinations of them are not synthesised on the fly. It is a real limit, named in the open rather than papered over, and it is exactly the kind of thing the next essays are for.

The cage holds. Then it doesn’t, in the one way a cage can’t.

I would like to end on the cage snapping shut, but the honest ending is better, and it is the reason I trust the project more, not less.

The same adversarial sweep that found no smuggled content in the source found something else. Two paths through the agent’s own deliberation arithmetic had no frozen test that could falsify them. A refactor, at some earlier point, had turned certain identity checks into definitions — so the tests that were supposed to pin those paths down had quietly become tautologies, true by construction, incapable of failing. The model never violated a test. It did something a cage cannot prevent: it made a test vacuously true. Constraining what can be written does not, by itself, keep what is measured meaningful. A grammar can make the wrong program unsayable; it cannot make a hollow test ring hollow. Someone has to keep looking.

The project has a smaller version of the same lesson embedded in its own closing document, and I find it the most honest thing in the repository. The final write-up ends with a block of commands a reader is meant to run to verify every claim. One line of that block was wrong — it stated an expectation that the block’s own execution then refuted. And the write-up notes, against itself, which line it was: “the one sentence of the block drafted from memory instead of derived from the frozen artifacts was the one that went wrong.” The single place the author trusted recollection over the mechanism was the single place the mechanism had to catch him.

That is the whole argument, compressed. What you write down, you drift from. What you can merely say, you get wrong — usually at the exact spot you were most sure. The remedy is not a better constitution or a longer prompt or a more disciplined author, human or model. It is to arrange the language so the wrong thing cannot be said at all, and then — because even that is not enough — to keep a test pointed at the places the grammar cannot reach. Cornering is the first half. Not trusting the corner is the second.