Behavior programs that know how likely they are.

Ordinary programs do what they say and nothing else. If you want to know how likely a program is to reach some state, you have to build a second thing beside it: a model, a simulator, a statistical estimate from many runs. The program and the model drift apart the moment one of them is edited, and neither can tell you that the other is wrong.

The idea here is to refuse the split. A program is written as a catalog of rules over a state that is a bag of resources: each rule says what it consumes and what it produces, and carries a weight. Whenever several rules could fire, the weights say how likely each is. That single addition changes what the text is. The same rules, read one way, are an executable: pick a rule, fire it, repeat. Read another way, they are a model: every possible sequence of firings is a run, and the weights give every run a probability. There is no second artifact to keep in sync, because the model is the program.

What that buys, concretely:

• A run can be priced. Any trajectory, your own or one the world hands you, has a likelihood under the program. So "was that expected?" is a number, not a feeling.
• Surprise becomes a defined event. If the world does something the program gives zero or near-zero probability to, you know it, at the moment it happens, and you know which rule or which missing rule is implicated. Debugging a model of the world turns into reading a diff.
• Consistency is checkable. Because every rule is a typed resource transaction, a wrong rule often fails before it runs: it consumes what cannot exist, or produces what nothing can consume. Many modeling errors become type errors.
• Learning is local. The structure of the world is written by a person; only the weights are fitted from data. When the fit is bad, you can see which rule's weight is off, instead of staring at an opaque loss.
• Exactness where it is affordable, sampling where it is not. Because the set of runs has a known shape, you can compute likelihoods exactly for small worlds and fall back to seeded sampling for large ones, and you always know which of the two you got.
• Behaviour stays a text. The thing that decides what a device does is a file a person can read, diff, approve and version. Improvement is a change to the file, not a retraining.

Start with the logic. Classical logic is about truth: a fact, once true, stays true, and you can use it as often as you like. That is the wrong logic for the physical world, where a cup of water used is a cup of water gone. Linear logic fixes this by treating facts as resources. A rule A, B ⊸ C does not say "if A and B then C"; it says "consume one A and one B, produce one C." A state is a multiset of such resources, and running the program is finding a proof: a sequence of rule applications that transforms the starting multiset into another. Every run is literally a derivation in the logic, and the logic guarantees that derivations respect conservation: nothing is used that was not there.

Now the probability. A proof search has choice points: several rules apply, and the logic alone does not prefer any. Classical proof search resolves them by strategy; here, each choice is a random draw with the rules' weights as odds. A run is a path through a tree of choices, and its probability is the product of the choices along it. Summing over all paths, the program defines a probability distribution on its derivations. That is the whole construction: logic supplies the space of possible histories, probability supplies a measure on it.

Two consequences are worth seeing clearly. First, this is exactly the mathematics of mass-action kinetics: rules are reactions, resources are molecules, weights are rate constants. A chemist would recognize the state space immediately, and the same machinery that gives chemistry its master equation gives these programs their measure. Second, the measure is on histories, not on states. Two runs that reach the same final state by different routes are different events with different probabilities. That is more information than a state-based model holds, and it is why a trajectory the world hands you can be priced as a whole.

There is a subtler point about what counts as "the same run." Two firings that do not touch each other's resources could have happened in either order, and nothing in the world distinguishes the orders. The honest object to assign probability to is the causal shape of the run, with independent firings unordered, rather than one arbitrary serialization of it. When a program's rules are such that this quotient is well-defined, the measure descends to it: runs weigh their causal structure, not their interleavings. That is where logic earns its keep: the proof-theoretic view sees the causal structure directly, where a simulator only ever sees one interleaving at a time.

The old objection to logic in the real world was that logic decides truth, and the world does not deliver truths; it delivers noisy, partial, surprising observations. A rule-based system that insists on truth either refuses to act or acts wrongly with full confidence.

This approach dodges the objection by changing what the logic is asked to do. It is not asked to decide what is true. It is asked to enumerate what is possible and to say how likely each possibility is. Uncertainty enters in two places, and both are explicit in the text. At every choice point, the weights encode the program's own uncertainty about what it will do next. At the boundary with the world, some rules consume resources the program never produces: observations that arrive from outside. Those rules carry weights too, so an observation is not a truth that overrides the model; it is an event the model had a price for. If the price was reasonable, the run continues and the likelihood updates. If the price was zero, the model was wrong in a specific place, and that place is named.

So: yes, uncertainty is anticipated, but only within the vocabulary the program has. This is the honest limit. The program cannot be surprised by something it has no word for; an observation outside its predicate set is not "unlikely," it is unrepresentable, and detecting it needs machinery outside the measure. Likewise, the weights are only as true as whoever fitted them, and a model can be smoothly, confidently wrong if its rules are the wrong rules with well-fitted rates. What the approach guarantees is not correctness but accountability: when the world and the program disagree, the disagreement is located, priced, and expressible as an edit.

Is it a solution to the logic-versus-uncertainty problem, a step, or a different form of computation? I would say all three, in different senses.

• It solves a specific version of the problem: a deterministic executable and a probabilistic model of the same behaviour are, by construction, the same object, so they cannot disagree. Everyone who has maintained a controller and a separate simulator of it knows what that removes.
• It is a step on the larger problem, because it fixes the vocabulary in advance. The open-world problem, finding out that your predicates are the wrong predicates, is not solved by a measure over proofs; it is moved to the loop around the program, where a person or a model proposes new rules and a gate decides whether to admit them. The measure makes that loop possible, by telling you when and where you need it, but it does not close it alone.
• And it is a different form of computation, in that execution and inference are the same act. Running the program forward is sampling a proof; scoring a trajectory is weighing a proof; learning is adjusting the weights on proofs you have seen. A conventional program computes a result; this kind computes a result and knows how likely it was to compute it. That is a smaller thing than general intelligence and a larger thing than a planner. It is a behaviour that carries its own model of itself, which is what you need before anything can be made responsible for what it does.

That last point is the practical reason it matters for devices: a system that can say "this is what I expected, this is what happened, and here is the gap, in your own words" can be supervised, by a person or by something much less trustworthy than a person, without handing either of them the controls.