Toward a universal theory of interactive software
Every interactive program faces the same problem. It has to act on values it does not control, and those values arrive on the world’s schedule rather than the program’s.
There is no general theory of this problem. There are many partial theories, each developed for one kind of product, and building real software means stitching them together. A great deal of the effort of building software goes into those seams.
What if one model covered almost all interactive software? A program would be described once, and the features that are now built as separate services would follow from the description.
That has become possible within the last fifteen years. Work on conflict-free replicated data types (CRDTs) showed that people can change the same data on separate devices and merge their work without anyone ordering the changes first. With the CALM theorem, there is now an exact line between the computations that can run this way and the ones that must wait for agreement.
The theory in this post builds on those results. If it is right, interactive software stops being a collection of special cases and becomes one subject. The theory is small: four primitives, and nine principles grounded in constraints that are true of all interactive software.
Four primitives: choices, resolvers, records, and functions
A running program alternates between computing and waiting for input. Computing is deterministic: the same inputs give the same outputs. Waiting happens where the program needs a value that its code does not determine. The theory names the point where the program waits, the source of the value, the stored value, and the computation.
-
A choice is a point where a run needs a value from outside its code. The program specifies what the value must satisfy, but not how the value is produced. Every input to a program is the value of some choice, so choices include form fields, button presses, sensor readings, random draws, clock readings, and replies from other systems. Each choice has:
- a stable identifier: the name of the declaration in the code that opens the choice, and the choice’s address, its position in the run that opened it;
- a view: the information presented to whatever supplies the value;
- options: the set of values the choice accepts;
- a timeout: how long the choice waits for a value;
- a default: the value used when the timeout passes.
A choice is open until it has a value. One declaration can open many choices, such as one question per guest or one per pass through a loop, and each has its own address.
-
A resolver supplies a choice’s value. A resolver can be a deterministic function, a random number generator, a sensor, a person, an AI model, or another program, such as another organization’s system, with choices and records of its own. A binding states which resolver supplies the value for which choice, and only a value from the bound resolver counts.
-
A record stores one choice’s value with its provenance: the choice, the resolver, the program version, the time, and the snapshot, which is the set of records available where the view was computed. The snapshot and the version determine the view, so the view can always be recomputed. Records are never modified.
-
A function is a deterministic map from a set of records to a value: the same records always give the same result. Everything other than records is the output of a function, including current state, screens, search indexes, metrics, access rules, and the set of open choices.
Choice names the open question and record names the answer. This post avoids the word “decision”, which is commonly used for both. Resolver names a role and implies no deliberation: a thermometer resolves the choice “current temperature”, and a random number generator resolves the choice “which variant this visitor sees”.
A record is a claim made from one perspective: it contains the value one resolver supplied, given the view that resolver was shown. The claim can be wrong, because a person can mistype a name and a sensor can drift. Records are never modified, and each choice has at most one record, so a wrong record is corrected by the record of a later choice, such as an edit, whose record names the record it supersedes.
Snapshots order the records. One record precedes another when it is in the other’s snapshot, or precedes a record that is, and two records are concurrent when neither precedes the other. The records therefore form a history ordered by what was available where each value was supplied, not a sequence ordered by one clock. Because records are only appended, a snapshot is everything up to a position in each place’s records, so a record stores those positions instead of a copy. They are usually one or two numbers (record fields).
The theory has no primitive for state. State is a function of the records, so state can always be recomputed, and two devices that store the same records and run the same program version compute the same state.
The view
A choice’s view and options form its boundary with the resolver. The view is everything presented to the resolver, and the options are every value the resolver can supply in return. Both are outputs of functions, computed from the choice’s snapshot under the program version, so a record identifies its view by those two fields and never stores the view itself.
A view is information, not its presentation. The same view can be drawn on a screen, read aloud by a voice interface, or given to an AI agent as a typed schema, and where a part of the view appears on a screen depends on the presentation, not on the view.
Nothing that crosses the boundary elsewhere appears in the records. A deterministic resolver reads only its view and options, and a randomized resolver reads them and a recorded seed. An opaque resolver also reads outside information, such as a person’s memory and conversations or a model’s training data, and an agent can act through channels other than the program’s choices. Four limits stated later in this post follow from this one fact:
- an estimate of how an alternative resolver would have performed is unbiased only when no outside information affected both a value and its outcome (goals principle);
- counterfactual replay is exact only until the first opaque resolver that the change could reach (goals principle);
- coupling through outside information, such as two people in different variants of an experiment talking to each other, appears in no function (coupling principle);
- a binding sets an AI agent’s authority only when the agent acts through the program’s choices (binding principle).
How a resolver differs from a function
A deterministic function can serve as a resolver, so a function and a resolver can run the same code. They differ in what happens to the output:
- A function’s output is derived. The output is computed from the records whenever the output is needed, and it is never stored as a record. Changing a function’s code changes every output the function computes from then on, including outputs about the past.
- A resolver’s output is recorded. Once a resolver supplies a value, later computation reads the record and does not run the resolver again. Changing a resolver changes only the values it supplies afterward.
A price shows the difference. If the price of an order is a function of the catalog’s records, a change to the pricing code changes the computed price of every past order. If the price is a choice bound to a pricing function, the quoted price is recorded, and each order keeps the price it was quoted after the pricing code changes. Whether a value should be a function output or a choice depends on whether the value must stay fixed after being shown to someone.
Resolvers ordered by determinacy
Of the ways resolvers differ, determinacy sets what can be learned from their records.
| Determinacy | Examples | Repeating the choice | Probability of the supplied value |
|---|---|---|---|
| Deterministic | a pricing function, game physics, a routing table | gives the same value | 1 |
| Randomized | A/B assignment, a bandit algorithm, a seeded shuffle | gives the same value with the same seed | known, and recorded |
| Opaque | a person, an AI model, a payment network, a sensor | may give a different value | unknown |
Opaque resolvers sit outside the system boundary, the line between what the program determines and what it receives from its environment. Whoever models a system sets where the system boundary runs, and engineering work moves resolvers across the boundary:
- automation replaces an opaque resolver with a deterministic one;
- a test suite replaces every opaque resolver with values written into the test in advance or recorded from earlier runs, so that runs can be reproduced;
- delegation to an AI agent replaces one opaque resolver with another.
An AI model sampled at temperature zero is deterministic in principle. In practice, batching, hardware differences, and model retirement make such a model’s outputs hard to reproduce, so this post classifies AI models as opaque. Another program is opaque unless its code is part of the model, and once its code is included, its choices and records are part of the system.
Some opaque resolvers have goals of their own: people, AI agents, and other organizations. These agents adapt to the program, so the program’s design changes the values they supply. Bidders on auction sites, for example, bid later when auctions end at a fixed time than when auctions end after a period with no bids. A sensor does not adapt to the program in this way.
The primitives in formal terms
A choice is a tuple
where:
- is the collection of possible sets of records;
- is the choice’s stable identifier, made of its declaration’s name and its address;
- computes, from a set of records, the view shown to the resolver, a value of type ;
- computes, from a set of records, the admissible values, a subset of the choice’s value type ( is the set of all subsets of );
- is the timeout;
- is the default, recorded when the timeout passes.
A record of choice contains , a value , the resolver, the version, the time, and the snapshot , a set of records that existed where the view was computed. The view the resolver was shown is , evaluated under the record’s version. Snapshots define a partial order: when or for some .
A binding maps each choice to a resolver. A resolver selects a value in given . A deterministic resolver is a function of the view and the options, a randomized resolver is a probability distribution over the options for each view , and an opaque resolver is one whose distribution is not part of the program. A function is a map for some output type . The view, the options, and the binding are themselves functions, so they change as records arrive.
In programming-language terms, a choice is an algebraic effect: an operation a program performs, whose result is supplied by a handler defined outside the code that performed the operation. A resolver is a handler that supplies one value per choice, and the value is recorded. Interaction trees give whole programs a semantics in these terms. A program denotes a possibly infinite tree whose nodes are requests to the environment and whose branches are the possible responses. A run is a path through the tree, and the records list the responses along the path.
Nine principles
Each principle starts from a constraint that is true of every interactive system and states a rule that meets it. Together the rules keep results agreeing across devices, surviving failures and releases, and arriving in time; keep each value referring to what its resolver was shown; and let resolvers be replaced and compared. They do not guarantee progress: every choice ends at its timeout, but a flow can keep opening new choices, such as a new reconciliation choice for an unknown payment each time the last one times out, until the network replies. The sections that follow explain each constraint, state the principle precisely, and list what follows from it.
| Principle | Constraint it addresses | What it requires |
|---|---|---|
| Derivation | Only values supplied at choices carry new information. | Store every value supplied at a choice, and compute everything else from the stored values. |
| Binding | Different resolvers can supply the same choice. | Specify each choice without naming its resolver, and set separately which resolvers may supply it. A record counts only if its resolver was bound and its value is among the options. |
| Sealing | Records reach different places at different times. | Conclude that a record does not exist only over a sealed scope. |
| Prediction | A response can be needed sooner than records can travel. | When the response deadline is shorter than the time to seal, show provisional values, and treat a record made from a provisional view as provisional too. |
| Effects | Presenting a choice can change the world, and the reply can be lost. | Present each choice under its identifier so that a repeat has no further effect, open a choice with effects only from final values, and make “unknown” the default when the reply can be lost. |
| Coupling | Functions combine records from more than one resolver. | Derive which choices affect each other from the functions, and use that one graph to place sequencers, sync, and experiment units, and to state what access rules must cut. |
| Grounding | Resolvers see the same things through different views. | Interpret each value against the view it was selected from, and record any interpretation that the view does not determine as a choice of its own. |
| Goals | Bindings can be ranked only against a direction. | State each goal as a function of the records with a direction and guardrails. |
| Versions | The program changes while its records persist. | Store the program version with every record, and translate old records instead of rewriting them. |
Derivation: store supplied values and compute everything else
Functions are deterministic, so the only new information that enters a running system is the values supplied at choices. Every other value can be computed from the records of those values. A table’s current row, a cache, a search index, and a dashboard are outputs of functions, and each one can be recomputed from the records. When a stored value disagrees with what its function computes from the records, the stored value is wrong.
Derivation principle: store every value supplied at a choice as a record, and compute every other value from the records.
Chess notation already follows the principle. A game is recorded as its move list, every position in the game is computed from the move list, and statistics about an opening across millions of games are functions over millions of move lists.
The real-time strategy game Age of Empires (1997) applied the principle to networking. Its developers calculated that sending each unit’s position, status, action, facing, and damage over a 28.8 kbps modem would limit a multiplayer match to about 250 moving units. Instead, each machine sent only its player’s commands, and every machine ran an identical deterministic simulation from the same commands, so the network traffic no longer grew with the number of units. The developers titled their account of the design 1500 Archers on a 28.8. Real-time strategy games have used this architecture, called deterministic lockstep, since the 1990s, and their replay files are lists of commands. Most web applications do the opposite: a server sends clients its current state, such as rows, documents, or rendered pages, and keeps the inputs that produced the state only in logs, if at all.
Several features follow:
- The data schema is the list of choice declarations. Every value the program received is in its records, so the events of an analytics tracking plan can be generated from the program’s choice declarations, and its metrics from the goals.
- Version history, audit, and debugging by replay are functions over the records. Undo appends a record that reverses an earlier one.
- Caches and indexes are stored outputs of functions. Keeping them current is incremental computation.
- Sync sends records, and offline work collects records on the device until they can be sent.
How choices are defined determines what is recorded. A drag gesture, for example, can be defined as one choice whose value is the point where the drag ends, or as a series of choices, one for each position sampled at 120 Hz. A value supplied by a deterministic resolver could be recomputed instead of recorded. Recording the value costs little and keeps the records interpretable after the binding changes.
Because records are never modified, deleting a person’s data on request needs a separate method: encrypt each person’s records under a key of their own, and destroy the key on request. Erasure is the one exception to recomputation and to finality: an output computed from erased records, even a final one, can no longer be recomputed as it was. The erasure request is itself a record, so the historical reading shows where records were erased.
Binding: specify each choice separately from its resolver
The lead story on a news site’s front page was once chosen by an editor. Today the same choice can be resolved by:
- a 50/50 assignment between two headlines;
- a bandit algorithm that shifts traffic toward the headline with more clicks;
- an AI model that selects a headline per reader;
- an AI agent that writes a new headline.
The view, the options, and the timeout stay the same, and only the resolver changes.
Binding principle: specify each choice (its view, options, timeout, and default) without naming a resolver, and set the resolver by configuration, in a binding. A record counts only if its resolver was bound to the choice and its value is among the options, both as of the view the resolver was shown. A default recorded at the timeout counts even outside the options.
With one specification per choice and a separately configured resolver, several features become one construct:
| Usual name | Resolver bound to the choice |
|---|---|
| conditional, feature flag | a fixed function |
| A/B test | uniform or balanced randomization |
| bandit | a randomized policy that learns toward a goal |
| personalization, recommendation | a function of the view learned from data |
| classification, routing | an AI model |
| delegation | an AI agent |
| the user interface | a person |
Changing a binding accounts for more features:
- Automation moves a choice from a person to a function.
- Escalation moves a choice back to a person.
- Delegation moves a choice from a person to an AI agent, under limits the person sets.
- Testing binds values written into the test or recorded in earlier runs, randomized resolvers that search for failures, and AI models playing personas.
- Presentation depends on the resolver. The same choice can be drawn on a screen, read aloud by a voice interface, or given to an AI agent as a typed schema. An API for agents is the set of a product’s choices with the rendering removed.
The choice with the largest effect on a product is which step comes next, and products are usually named after the resolver bound to that choice:
- When a deterministic function selects the next step, the product is an interview, such as a tax questionnaire or a checkout.
- When a person selects the next step, the product is a workspace, such as a spreadsheet.
- When an AI agent selects the next step, the product is a delegated task, such as a coding agent working through a repository.
Mixed-initiative interfaces move the binding of the next-step choice between a person and a program within one session.
Two properties of a binding limit what an AI agent can do:
- Discretion is the number of outcomes that the choices bound to the agent can reach. “Select one of three refund amounts” allows little discretion, and “reply to the customer” allows a great deal. Splitting a choice with a large option set into choices with small ones makes each part checkable, and lowers discretion when some parts are bound to someone else, so how finely a task is divided and bound sets how much autonomy an agent has. Levels of automation can be set separately for gathering information, analyzing the information, selecting an action, and carrying the action out, which amounts to one binding per stage.
- Authority is the set of choices bound to the agent. Authority is set by the binding, independently of what the agent is capable of, provided the agent can act only through the program’s choices, a point developed in Old Foundations, New Agents.
The binding is the program’s only rule for who may supply a value. Releases, seals, and records that a binding reads, such as a grant of a role, are values supplied at choices too, so the question of who may do any of them has one answer: whoever is bound to that choice in the version in force. A value from a resolver that was not bound, or outside the options offered, is recorded as refused, and no function other than an audit reads it. Checking that a record really came from the resolver it names is a matter of signatures, not of the theory.
Determinacy also sets what the records can contain. A randomized resolver can record the probability with which it selected the value, called the propensity in causal inference. A person’s propensities are unknown, and a person cannot be asked the same question again with nothing else changed. The goals principle depends on this difference.
Sealing: wait for every record that could arrive before concluding that one is absent
Records reach different places at different times, so the snapshot from which one view is computed can lack records that another place already holds.
“These people have voted” and “this document contains these edits” only grow as records arrive, so an output computed early is later added to but never retracted. Such a function is monotone:
Here and are sets of records, is a function, and is the order on ‘s outputs, such as inclusion for sets.
Other functions conclude that some record does not exist:
- “the seat is free”;
- “the latest price is 40”;
- “this username is available”;
- “candidate A won”.
One late record can make such a conclusion false. A value is final when no record that can still be admitted would change it. The conclusion can be final only if the system waits until every record that could affect the conclusion has had time to arrive, and then refuses any record that arrives later or admits it into a later scope, where it acts as a correction. Three terms describe how a system closes that waiting period:
- A scope is a set of records picked out by a condition, such as every booking for seat C14 at tonight’s performance.
- The sequencer of a scope is the single resolver that admits records into the scope, one at a time and in one order. Each scope that needs an order has exactly one sequencer at a time.
- A seal is a record, written by the sequencer, stating that the scope is complete up to some position in that order: no record will later be admitted at or before that position. Admitting a record also seals the part of the scope before the admitted record, which is how a sequencer settles which of two concurrent bookings came first. A scope can also be split into a fixed set of parts whose records never need ordering against one another, each with its own sequencer, as the escrow method below does. The whole scope is then sealed as far as every part is, as an election’s ballots are complete once every precinct has sealed its own.
Sealing principle: later records only add to a monotone function’s output over admitted records. A conclusion that depends on records being absent is final only over a sealed scope.
The CALM theorem draws the same line for queries, whose outputs are sets ordered by inclusion. When no place holds information about how records are divided among places, a query has a consistent distributed implementation that needs no coordination if and only if the query is monotone. Even “the current value” is a conclusion about absence, as is any value that a correction or an undo could supersede: last-writer-wins replication orders writes by timestamp, but no replica can rule out a later write.
Seals appear at every scale under other names:
| Usual name | Scope | Sequencer |
|---|---|---|
| Pressing submit | one person’s answers on a form | that person’s device |
| A hold’s timeout | one held seat | the booking system |
| A step of a lockstep simulation | every participant’s input for one step | the simulation’s host |
| A transaction commit | the rows the transaction read and wrote | the database |
| An entry reaching consensus | one position in a replicated log | a quorum of replicas |
| A watermark in a stream processor | one input’s events before a timestamp | that input’s source |
| An analysis cutoff | the data for one experiment | the experimenter |
| Closing the books | one accounting period | the accounting department |
| Polls closing | one precinct’s ballots | the precinct’s officials |
The smallest scope is one choice. A choice with a timeout can receive both its resolver’s value and its default, and each can be admitted alone but not both, so each such choice is a scope with a sequencer of its own, which runs the timer, admits whichever value reaches it first, and refuses duplicate replies.
The sealing method changes what agents do. A study of online auctions compared eBay, where auctions ended at a fixed time, with Amazon, where auctions continued until ten minutes passed without a bid. Bids in the final seconds were far more common on eBay. Bidders with more experience bid later on eBay and earlier on Amazon. The sealing method worked as a mechanism in the game-theoretic sense: the method set the incentives, and bidders adapted to the method.
Two methods avoid waiting for a sequencer:
- Use choices whose records always merge. Operations are invariant-confluent when any two valid sets of records they produce from a common valid set merge into a valid set. Likes on a post are invariant-confluent, and seats in a theater are not.
- Split the scope. The escrow method divides a shared quantity into shares, and each share has its own sequencer. A box office holding a block of seats can sell those seats without contacting the central system, and a warehouse can promise its own stock.
Splitting works because coordination is needed only between places. When every record that a conclusion about absence depends on is admitted at one place, the sequencer there writes the seal alone, and no other place takes part. Ameloot and colleagues made this precise for queries. When every place can test which place a given record is assigned to, which they call the policy-aware setting, the queries with coordination-free implementations are exactly the domain-distinct-monotone queries. A domain-distinct-monotone query’s output may shrink when a new record mentions only values already present, but not when a new record mentions a value never seen before. The class contains every monotone query and more, so information about where records are placed moves the CALM theorem’s line.
The sealing method also sets what a statistical conclusion means. A fixed-horizon significance test assumes that its cutoff, which is a seal, was chosen without reading the outcomes. Sealing once the result looks significant reads them, and false positives multiply although the scope is sealed. Always-valid inference stays valid at any cutoff, however it was chosen.
Polarity and strata
A function can be monotone in some of its inputs and not in others. The live holds on a seat are the holds on that seat minus the released ones. A new hold can only add to the live holds, and a new release can only remove from them, so the function that computes live holds is monotone in the holds and antitone in the releases. Only the releases must be sealed before a hold in the output is final. Each input of a function therefore has a polarity:
- positive, when more records in the input can only add to the output;
- negative, when more records in the input can only remove from it;
- unknown, when no analysis establishes either, as for most general-purpose code.
Polarities compose like signs. “This seat has no live hold” is antitone in the live holds, which are antitone in the releases, so the conclusion is monotone in the releases: a new release can only make the seat free. The conclusion is antitone in the holds, so only the holds must be sealed before “free” is final.
A program’s functions form a directed graph, the function graph, from the records to every view and every open choice. Each edge connects an input to the function that reads it and carries that input’s polarity. Removing the negative and unknown edges divides the graph into strata, parts in which every function is monotone in its inputs. In Datalog, this structure is called stratified negation, and stratification is how monotone and non-monotone parts compose into one program. An output is final when every scope read through a negative or unknown edge on the output’s paths is sealed up to the positions the output depends on, so coordination is needed only at those edges.
Monotonicity is also relative to the order chosen for a function’s output. “The latest price” is not monotone under inclusion, because a later price replaces an earlier one. Ordered by the position of the write that set the price, the same value only moves forward, and a last-writer-wins register uses that order. An order in which any two values have a least upper bound, and merging two replicas computes that bound, is a join-semilattice, and every state-based CRDT is defined over one. What becomes final under such an order is a bound, such as “the price was set at write 41 or later”, not the conclusion that no later write exists. A test on a growing value, called a threshold test, is final once true only when every larger value also passes it: “at least 100 likes” is such a test, and “exactly 100 likes” is not. BloomL is a language whose values are lattices and whose monotone functions and threshold tests a compiler can check.
Finality relative to scopes
A value is final relative to the scopes whose seals it rests on, and one value can be final relative to one scope and provisional relative to a larger one. A card payment is final once the card network settles it, and a dispute can still reverse it until the dispute window closes. The window’s end is a seal of its own, written by a timeout. Any function whose output can change only within a known period, such as a count of events that may arrive late, is sealed the same way at the period’s end, so the output is provisional until a known time rather than indefinitely. In stream processing, such a period is called allowed lateness.
Admission has the same structure. An admission held only in a sequencer’s memory is lost if the sequencer fails before storing the admission, so an admission is final only once stored where it survives the failures its scope must survive. Finality therefore comes in tiers, such as admitted on a device, stored on a quorum of servers, settled by another organization, and past a dispute window. Each tier is a seal, and a view can present each tier differently.
Prediction: show provisional values when records cannot arrive in time
Each choice involves two durations:
- The response deadline is the longest time that can pass between supplying a value and showing its consequence before the interaction fails, for example because a game stops feeling responsive or a person concludes that a button did nothing.
- The sealing latency is the time between supplying a value and the arrival of the sequencer’s admission at the place where the value was supplied. The sealing latency is at least the round trip to the sequencer.
Human perception and physics set both durations. Responses within about 0.1 s feel immediate. Animation at 60 Hz needs a new frame every 16.7 ms. For telephone calls, ITU-T Recommendation G.114 recommends at most 150 ms of one-way delay. On the other side, light in optical fiber travels about 200,000 km/s, so each 100 km of fiber adds about 1 ms to a round trip before any routing or processing. A sealed result within one 60 Hz frame needs the sequencer within about 1,700 km of fiber, and a round trip between London and Sydney over fiber takes at least 170 ms.
When the response deadline is shorter than the sealing latency, the view has to include records that the sequencer has not yet admitted. Functions evaluated over those records give provisional values, which are replaced when the sequencer’s admissions arrive.
Prediction principle: when a choice’s response deadline is shorter than its sealing latency, show provisional values computed from records not yet admitted, and recompute them when the admissions arrive. A record made from a view that showed provisional values is provisional too.
Several familiar features are this one mechanism:
- optimistic updates in a web app;
- characters appearing as they are typed into a shared document;
- a shooter’s client moving the player before the server confirms the move;
- rollback netcode in fighting games;
- the pending line in a banking app after a card payment.
In the card payment, the pending line is a provisional value computed from the authorization, and settlement days later is the seal that posts the payment.
For invariant-confluent choices, the device admits the record itself, so monotone outputs over it are final at once. For other choices the provisional value can be wrong. The cost of prediction grows with how often provisional values are wrong, because each wrong provisional value becomes a correction that someone sees.
A provisional value can also reach a record. A person who holds seat C14 provisionally and then adds a meal for C14 makes the meal record from a view that showed the hold. If the sequencer refuses the hold, the meal record rests on a record that was never admitted, which rollback recovery calls an orphan. Its choice states what happens then: the record is refused, the choice is asked again, or the value is applied again on top of the admitted records, as rollback netcode replays a player’s inputs.
Designers have three levers:
- Move the sequencer closer. Trading firms place their servers in the exchange’s data center, and a drawing app makes the device the sequencer for its own strokes.
- Lengthen the response deadline. Age of Empires scheduled each command to run two 200 ms communication turns after the command was issued. Turn-based games make the deadline a whole turn. EVE Online slows its simulation to as little as 10% of normal speed during large battles.
- Make the choice invariant-confluent, so that the choice needs no seal.
Optimistic simulation with rollback is the general form of prediction. Each part of a simulation runs ahead using the records available to that part, and when a record arrives with an earlier timestamp, the part rolls back and recomputes.
Effects: present each choice so that a repeat changes nothing
Presenting a choice to a resolver outside the system boundary can change the world. A request to a card network moves money, a message to a mail server reaches a person, and a request to a deployment service changes what people run. The presentation and the record of the choice are separate events, and a run can fail between them: the card network approves a charge, and the reply is lost or arrives after the timeout. The derivation principle covers replay, because later computation reads the record instead of presenting the choice again. It does not cover a retry before any record exists, or a default recorded after the world has already changed.
Effects principle: present each choice under its stable identifier, so that presenting it again has no further effect; open a choice that has effects only from final values; and when the reply can be lost, make “unknown” the default.
Each part uses something the theory already has:
- The choice’s identifier is the idempotency key. Payment networks and many APIs accept a key with each request and return the first result when a key repeats. A retry presents the same choice, so it carries the same key.
- Effects follow final values. A provisional value can be wrong, and a sent email cannot be unsent, so a confirmation is opened only after the booking it confirms is admitted. An effect that must start sooner is split, as a card authorization holds funds when a trip is requested and the capture waits for the final fare. A compensating choice, such as a refund, is an effect too, and opens from the final record that calls for it.
- “Unknown” is an option. A default of “declined” for a payment is wrong whenever the network approved the charge and the reply was lost: the program releases the seat and keeps the money. A default of “unknown” opens a second choice, bound to the same network, whose value is the outcome under the first choice’s identifier, and a late reply to the first choice supplies that value. If the second choice also ends in “unknown”, a person decides.
Whether a choice has effects is a property of the choice, not of its resolver. The same card network resolves a balance inquiry, which has no effect, and a charge, which has one.
No method performs an effect exactly once through a system that ignores the key. After a lost reply, the sender cannot determine whether the request arrived, which is the two generals problem. The principle therefore gives one effect per choice where the resolver has committed to keeping the identifier for longer than the choice’s timeout (see commitments), and a recorded “unknown” everywhere else.
Coupling: derive which choices affect each other from the functions
Functions combine records supplied by different resolvers, so the value supplied at one choice can change the view or the options of another choice. Two relations describe how choices affect each other. In the definitions below, and are choices, and are records of values supplied at them, and are the view and option functions of , and is an invariant, a condition every admitted set of records must satisfy. ranges over , the reachable sets of records: those a run of the program can produce, each of which satisfies .
Read coupling holds when a record from can change ‘s view or options:
In words: for some reachable set of records, adding some record from changes what shows or accepts.
Order coupling holds when records from and can each be admitted alone, but not together:
In words: for some reachable set of records, adding either record alone keeps the invariant true, and adding both makes the invariant false.
Order-coupled choices need a sequencer to admit one record first and refuse the other. Sets of records merge by union and each admission adds one record, so a set of choices is invariant-confluent exactly when no order coupling holds among them: a failure over longer histories always contains a failing pair. Order coupling can hold without read coupling. When ‘s options ignore ‘s records, as a sign-up form that accepts any email address does, the sequencer refuses ‘s record at admission.
Two people booking the same seat are order-coupled. Two people commenting on the same post are read-coupled. Two people typing into the same paragraph of a shared document are read-coupled when a merge algorithm combines their edits, because every combination of concurrent edits then merges into a valid document, though not always into the text either person meant.
Coupling principle: derive which choices affect each other from the functions, and use the resulting graph to set what is synchronized, which records share a sequencer, and which units share an experiment variant, and to locate the edges that access rules remove.
Each use cuts different edges: sequencer scopes keep order edges inside, experiment units keep read edges inside, and sync follows read edges. Exact derivation is undecidable for general code, so a compiler keeps an edge wherever a function, or a resolver that learns from records, reads another choice’s records. Extra edges cost coordination or statistical power, not correctness.
Most of what a product does about other people uses one of the two relations:
| Feature | Relation | Use |
|---|---|---|
| Subscriptions, interest management in games | read | deliver records along edges |
| Presence, live cursors | read | deliver along edges with short response deadlines |
| Notifications | read | deliver along edges with long response deadlines |
| Access rules, privacy settings, blocking | read | remove edges; the lattice model of information flow is the general form |
| Sharding | order | partition so each part has one sequencer; edges that cross parts need distributed transactions |
| Experiment units | read | partition so each part receives one variant; edges that cross parts carry treatment between variants |
The last row is where statistics and systems engineering meet. Causal inference’s stable unit treatment value assumption (SUTVA) includes the requirement that one unit’s outcome not depend on another unit’s treatment. Read coupling that crosses between variants can break the requirement, and so can outside information, such as conversation between units, which no function shows. Software rarely meets the requirement by default, so it has to be engineered. Three methods are in use:
- Partition the graph. Graph cluster randomization assigns variants to clusters of a social graph. The same year, balanced label propagation partitioned Facebook’s social graph across servers, so experiment units and shards can be computed from one graph.
- Randomize over time. When coupling runs through a shared pool, as when every rider in a city draws on the same drivers, the graph has no useful clusters. Switchback designs randomize time periods instead.
- Change the functions to remove edges. A budget-split design for ad experiments gives each variant its own share of every advertiser’s budget, so the variants cannot draw on the same money. This design is the escrow method from the sealing principle, used to obtain statistical independence instead of coordination-free writes.
An access rule removes an edge only when nothing in ‘s view, counts and refusals included, changes with ‘s records, the property called noninterference. Access rules can remove read coupling but not order coupling. If two people try to register the same email address, the second person learns that the first exists, whatever the access rules say, because the refusal itself carries the information. A sign-up form that reports “this email is already registered” therefore lets anyone test whether a person has an account. The standard fix moves the outcome to a channel only the address’s owner can read: “If an account exists, we have sent a link.”
Grounding: interpret each value against the view it was selected from
Resolvers see the same things through different views. A collaborator’s view of a shared spreadsheet differs from an AI agent’s when their snapshots differ, an access rule can hide a row from one of them, and a phone and a voice interface present the same view differently. A value that refers to something, such as “delete row 3”, “the later slot”, or a tap at a point on a screen, refers through the view it was selected from. Read against any other view, it can pick out a different thing.
Grounding principle: interpret every value against the view it was selected from. Resolve each reference to the identifier of the thing it picks out in that view, and when the view does not determine the thing, as with free text, make the interpretation a choice of its own, whose record the value’s author can see and supersede.
The name comes from grounding in communication, the process by which people in a conversation establish that they refer to the same things. The record already identifies its view by snapshot and version, so the principle needs no new storage. It needs identifiers that stay fixed when the view changes. Every thing a view shows was introduced by some record: a seat by the record that published the seating plan, a paragraph by the edit that created it, a row by its insertion. The identifier of that record names the thing in every view, whatever its position, presentation, or version.
Three methods meet the principle, in increasing order of cost:
- Options are identifiers. The presentation converts a tap or a click into the identifier of the thing under it, on the device where the presentation is known, and only the identifier is recorded. Sequence CRDTs give every character of a shared document an identifier for the same reason, so an insertion after a given character means the same on every replica.
- A function interprets the value against its snapshot. A position, such as “row 3” or “offset 12”, is read in the record’s snapshot and moved past every concurrent record. Operational transformation moves text positions this way. Shooter games apply the method to time: with lag compensation, the server evaluates a shot against the positions the shooter’s view showed, not against the positions when the shot arrives.
- A choice interprets the value. When the view does not determine the thing, as with “move my booking to the later slot” typed into a chat, a choice bound to an AI model or a function selects an identifier. Its view contains the original value and that value’s snapshot, and its record enters the author’s view, where the author can supersede it. A search engine that reports “showing results for” a corrected query uses this method, and so does an agent that states its reading of a request before acting on it.
Choices with effects make the third method costly to skip. An agent that reads “delete the old drafts” against the wrong view deletes the wrong files, and the effects principle allows no correction once the effect has started, so an interpretation that leads to an effect is shown to its author first. Plan reviews and approval prompts for AI agents are this step.
The principle matters more as presentations multiply. When an AI model composes the layout for each person, two people looking at one view see it arranged differently, and only identifiers let one of them refer to what the other sees. Grounding does for the things a view shows what stable identifiers do for choices: a choice keeps its identifier across retries and releases, and a thing keeps its identifier across views.
Goals: functions with a direction and guardrails
Several resolvers can be bound to one choice, and they can be ranked only against a direction. Systems are built to change something: more completed bookings, fewer refunds, faster answers. A goal states such a change as a function of the records, together with limits the change must respect. Formally, a goal is a function ( is the real numbers) to be increased or decreased, together with guardrails : functions that must stay within bounds while changes. Conversion rate is a goal, and refund rate, latency, and complaint rate are typical guardrails. The period over which a goal is evaluated belongs in its definition, because a metric that rises over a week can fall over a year. Guardrails can also carry what a design costs each resolver, such as how many choices a person is shown, how long each view is, and how many confirmations an agent requests. A goal that counts only the outcomes its operator wants treats every resolver’s effort as free.
Goals principle: state each goal as a function of the records with a direction and guardrails, and compute analytics, experiments, and optimization from that one definition.
Several practices are uses of goals:
- Analytics evaluates goals and their inputs over the records.
- Attribution follows provenance from a goal’s value back to the records it was computed from.
- An experiment combines four parts from earlier principles: a randomized resolver with recorded probabilities, a goal, units taken from a partition of the read-coupling graph, and a seal for analysis.
- Bandit algorithms and personalization models are resolvers that read a goal’s value while they run.
- Pre-registration records the goal, the analysis plan, and the rule that sets the cutoff before any outcome exists.
Recorded probabilities make it possible to evaluate a binding that was never deployed. The standard estimator, inverse propensity scoring, is
where:
- is the number of records of one declaration’s choices;
- is the view in the -th record, and is the value supplied;
- is the probability with which the deployed resolver selected , recorded at selection;
- is the probability that a candidate resolver would select given view ;
- is the outcome of the -th record, for a goal that averages one outcome per record;
- is the estimated value of that goal had been bound to those choices.
In words: reweight each recorded outcome by how much more or less often the candidate would have selected the same value. The estimate is unbiased when each is correct, gives a positive probability to every value might select in the same view, and no record’s value changes another record’s view or outcome. The second condition is why the records of a deterministic resolver, with probability 1 on one value and 0 on the rest, cannot evaluate alternatives without a model of the outcomes they never show. An opaque resolver’s probabilities can only be estimated, which assumes that no outside information affected both the value and the outcome. Offline evaluation of news recommendation applied a closely related replay method to a log of randomly selected articles, and a decision service built on the estimator records each probability at the moment of selection.
Counterfactual replay evaluates a change to one run instead of a binding’s average. Hold the functions fixed, change one record, and recompute everything after the changed record. The result is exact until the first later opaque resolver that the change could reach, through its view or through outside information. A pinned AI model can be asked again, but a person cannot and needs a stand-in, such as a model of the person’s behavior.
Optimizing a goal without guardrails tends to find the cases where the function differs from what the function was meant to measure, and a more capable resolver finds more of those cases. Experimentation practice limits the problem with guardrail metrics.
Versions: store the program version with every record
Programs change while choices are open. Some people still run last year’s version of an app, an insurance claim may be halfway through a review that takes weeks, and an AI agent may be partway through a task. If every record carries the version it was made under, each record can be read under the functions in force when the record was made.
Versions principle: store the program version with every record, and store each release as a record. A migration is correct when it gives the same state as recomputing from the records under the new version.
- A release is a record. It is admitted into a scope’s order like any other record, so every replica that reads the scope switches versions at the same position, and choices opened after that position use the new version.
- Migrations change how records are read. Old records stay as they are, and translation between versions is a function.
- Open choices carry over by stable identifier. A form can be edited while thousands of people are partway through the form, as long as every open choice maps to a choice in the new version or to a recorded fallback.
- Changing a binding’s definition is a release, because the change alters which resolver supplies each value. Changing an AI agent’s model is one case.
Whether a value is data or code depends on the functions that read it. A spreadsheet formula is a value supplied at a choice, and the functions that compute the sheet read it as code, so editing a formula is a release limited to one document. A release can therefore apply to one scope, and a record then carries the version of every scope whose functions computed its view.
Records can therefore be read in two ways, for two different questions. The historical reading evaluates each record under the functions in force when the record was made, and gives what a person was shown and why they selected what they did. The current reading evaluates every record under the newest functions, and gives what the state is now. Both are functions of the same records. A release changes only the current reading of a final value. A release that changes what a choice’s value means, rather than how it is written, gives the choice’s declaration a new name, because no translation turns a value with one meaning into a value with another. Open choices of the old declaration then receive a recorded fallback, which is “unknown” for a choice whose effect may already have started.
Rewriting stored state, as a database migration or a codemod does, is an optimization of the same idea, and its correctness condition is exact. Let compute state of type from a set of records reachable under version , let translate records made under into records that reads, and let migrate stored state from version to version . The migration is correct when
In words: the two paths around this commuting square, migrating the old state and translating the records to recompute the state under the new version, give the same result. A correct exists exactly when the old state keeps everything the new state needs: any two reachable sets of records with the same old state also have the same new state. A balance cannot be migrated to a count of transactions, because and have the same balance, and only recomputation from the records gives the count.
The records contain real past runs, so the condition can be tested by replaying those runs along both paths. Operator libraries such as schema modification operators, bidirectional lenses, and functorial data migration build and from parts that compose, but none of them establishes the square, which also depends on what the new version’s functions compute.
One requirement has no exception. If a release changes what an earlier view showed, after someone selected a value based on that view, the change must itself be recorded, as a restatement is in accounting. Otherwise the selection loses the context that gave it meaning.
Composition: programs as resolvers
A resolver can be another program. When a booking program binds its payment choice to a card network, the network receives the choice’s view and supplies a value from its options. Inside the network, the request is a choice of the network’s own, kept in the network’s records. The value appears in the records of both programs, linked by the first choice’s identifier.
Two programs bound to each other’s choices form one larger program. Its open choices are the open choices of the parts that neither part resolves for the other, and its coupling graph has edges between the parts: a seat hold in the booking program and a card authorization in the network are order-coupled, and the hold the authorization places on funds is escrow in the network’s scope. Polynomial functors give this composition an algebraic form, in which an interface is a set of positions, each with the set of replies it accepts. Here the positions are the open choices with their views, and the replies are their options. Interaction trees compose the same way.
Composition adds no principle, because every principle applies inside each program. It describes how programs connect, which the effects principle already assumes.
Commitments
A program can observe another program only through views and values, so it can rely on the other’s behavior only as far as the other has committed to that behavior. A commitment is a record whose value is a law over later records of the commitment’s own resolver. A card network’s commitment that a repeated key returns the first result for 24 hours is a law over the network’s replies. A program’s releases are commitments in the same sense: each one fixes, for the program’s own records, which resolvers count, which options are accepted, and which default is recorded at each timeout.
Three properties follow from the definition:
- A resolver can commit only its own records. A law over another resolver’s records is one the committing resolver cannot keep. Promise Theory starts from the same rule: an agent can promise only its own behavior.
- Commitments are checked against the records. A law that forbids something, such as two different replies under one key, is broken by records that exist, and stays broken, because records are never modified. A law that something happens by a deadline is broken by an absence, so by the sealing principle the breach is final only once the deadline’s scope is sealed, which the timeout of the corresponding choice does.
- The effects principle depends on commitments. One effect per choice requires the resolver to keep each choice’s identifier for longer than the choice’s timeout, which only the resolver can commit to. Through a resolver without that commitment, a lost reply can only be recorded as “unknown”.
Consent, terms of service, rate limits, data-retention policies, and service-level agreements are commitments. Parties that do not trust each other can still check each other’s commitments, against signed records.
How the terms of the theory relate
The matrix below relates eleven of the theory’s terms, primitives first, and states how each acts on the others. A choice’s view and options are parts of the choice, so they have no rows of their own. Each cell reads from its row to its column: the cell in row Resolver and column Choice reads “a resolver resolves a choice”.
Every filled cell lies on or below the diagonal, so no term acts on a term that comes after it. Several terms are cases of the primitives: a binding and a goal are functions, a sequencer is a resolver, and a seal, a release, and a commitment are records. Five principles add no term. Coupling is one cell: a function couples choices. For prediction, a provisional value is a function’s output that is not yet final. For effects, the key that makes a repeat harmless is the choice’s identifier, and “unknown” is one of the choice’s options. For grounding, a value refers through the view it was selected from, which its record identifies by snapshot and version. Derivation appears as an absence: no term denotes stored state.
The principles are independent: each can be broken while the other eight hold. The table gives one such failure per principle, with the two sentences of Binding taken separately, and what goes wrong.
| Principle broken | A failure in which every other principle holds | What goes wrong |
|---|---|---|
| Derivation | A seat count kept by handler code drifts from the bookings after a failed request. | a wrong result |
| Binding, first sentence | The payment choice names its card network, so a test cannot bind a scripted resolver. | changing a resolver needs new code |
| Binding, second sentence | Any signed-in user can approve a refund bound to the support lead. | an unauthorized result |
| Sealing | A results page declares a final winner before every precinct has reported. | a wrong result |
| Prediction | A game waits for the server before moving the player. | a late result |
| Effects | A retry after a lost reply carries a new key, and the card is charged twice. | a repeated effect |
| Coupling | An experiment randomizes riders who draw on the same drivers. | a biased estimate |
| Grounding | An agent’s “delete row 3”, read against the current sheet instead of the agent’s snapshot, deletes a different row after a collaborator inserts one above it. | the wrong thing changed |
| Goals | A bandit maximizes clicks while the declared goal is completed bookings. | the wrong target optimized |
| Versions | A workflow paused under one version resumes under the next and reads an old field with its new meaning. | a misread record |
Features built from the principles
| Feature | Principles | Construction in the theory |
|---|---|---|
| Version history, audit, undo | derivation | functions over the records; undo appends a reversing record |
| Caches, indexes, search | derivation | stored outputs of functions |
| Analytics, funnels, attribution | derivation, goals | goals and provenance over the records |
| Feature flags, A/B tests, staged rollouts | binding, coupling, goals | a randomized resolver with recorded probabilities, units from a partition of the read-coupling graph, and a goal |
| Personalization, recommendation | binding, goals | a learned resolver that reads a goal |
| Automation, escalation, delegation | binding | changing a binding, within rules on the binding table |
| Simulated users, regression replay | derivation, binding | resolvers that return values written into a test, or recorded values |
| Voice interfaces, accessibility, agent APIs | binding | one choice presented differently per resolver |
| Durable workflows, reminders | derivation, binding | open choices are functions of the records; timeouts record defaults |
| Submit buttons, turns, commits | sealing | seals |
| Pending and confirmed states | sealing | seals at several tiers of finality |
| Inventory, quotas, rate limits | sealing | escrow: a scope split into shares, each with a sequencer |
| Offline mode | sealing | admitting invariant-confluent or escrowed records on the device |
| Optimistic UI, client prediction, rollback | prediction | provisional values |
| Retries, idempotent payments, reconciliation | effects | presentation keyed by the choice’s identifier; an “unknown” default that opens a reconciliation choice |
| Permalinks, comment anchors, positions in shared text, lag compensation | grounding | references by identifier, or positions and times read in the record’s snapshot |
| Disambiguation, plan review before an agent acts | grounding | an interpretation choice whose record its author can supersede |
| Third-party APIs, webhooks, service-level agreements | effects | programs bound to each other’s choices; commitments checked against the records |
| Presence, live cursors, notifications | prediction, coupling | read coupling, delivered by response deadline |
| Access control, privacy, blocking | coupling | removed read-coupling edges |
| Sharding | coupling | a partition of the order-coupling graph |
| Experiments with interference | coupling, goals | a partition of the read-coupling graph, or functions that remove edges |
| Off-policy evaluation, counterfactuals | derivation, binding, goals | recorded probabilities and replay |
| Live updates, hot code loading, schema migration, old clients | versions | versioned records, releases that take effect at a position, and translation functions |
Six classes of choices by coupling and response deadline
Two quantities defined in the sealing, prediction, and coupling principles determine what a runtime must do for a choice:
- its coupling with choices in other runs: order-coupled if it has any order coupling, read-coupled if it has only read coupling, and independent otherwise;
- its response deadline: long (a second or more, enough for a network round trip) or short (below about 100 ms, shorter than many round trips).
| Independent | Read-coupled | Order-coupled | |
|---|---|---|---|
| Long deadline | compute anywhere; the device is the sequencer | merge, deliver later | wait for the sequencer |
| Short deadline | compute on the device | merge, deliver live | show provisional values, reconcile with the sequencer |
The runtime’s work grows from the top-left class to the bottom-right one.
The usual taxonomy of forms, editors, and games hides two of the classes. Comment threads, wikis, and email are read-coupled with long deadlines. Bookings, username registration, and bank transfers are order-coupled with long deadlines: they wait for a sequencer and do not predict.
Products combine classes, so the classes describe choices, not products. A ride-hailing trip uses four of the six:
| Choice | Resolver | Response deadline | Coupling | Runtime behavior |
|---|---|---|---|---|
| Destination | rider | long | independent | compute anywhere |
| Price quote | pricing function with a market-balance goal | long | read, through shared supply | merge, deliver later; experiments need switchbacks |
| Rider–driver match | dispatch function | seconds | order, over drivers | wait for a sequencer per zone |
| Accept the trip | driver | about 15 s | order | wait for the sequencer |
| Car on the map | GPS receiver | short | read | merge, deliver live; the view interpolates between samples |
| Message the driver | rider or driver | long | read | merge, deliver later |
| Payment | card network | long | order, over funds | wait for the card network; authorize at the request, capture the final fare |
| Rating | rider | long | read, through the driver’s average | merge, deliver later |
Groupware research classified collaboration tools by whether people work at the same or different times, and in the same or different places. The table above keeps that matrix’s shape and replaces both axes with quantities that determine the architecture: place becomes coupling, and time becomes the response deadline compared with the round trip.
Designs the principles rule out
- A sealed result for an order-coupled choice sooner than the round trip to its sequencer. A sealed result within one 60 Hz frame requires a sequencer within about 1,700 km of fiber. Anything faster is provisional.
- A final conclusion about absence over an unsealed scope. A record still in transit can make the conclusion false.
- An estimate of what launching a variant to everyone would change, from per-person randomization, when read coupling crosses between variants and no exposure model states how treatment spreads along it. The comparison then measures a mixture of direct effects and spillover, the expected average treatment effect, which differs from the effect of a launch.
- Exact counterfactual replay past an opaque resolver whose view would have changed.
- Hiding the result of an order-coupled choice from the party whose record was refused. An access rule can make the refusal less specific or send the refusal through another channel, but cannot remove the refusal.
- Changing what a past view showed without recording the change.
- Performing an effect exactly once through a system that does not deduplicate by identifier.
- Reading a reference against a view other than the one its value was selected from.
The same structure in five other fields
Several fields reached this structure independently and named its parts differently. The table pairs each term with its nearest counterpart in five fields, and each field contributed a result this post uses.
| This theory | Game theory | Reinforcement learning and control | Probabilistic programming | Databases and distributed systems | Causal inference |
|---|---|---|---|---|---|
| record | move in the history | logged transition | entry in an execution trace | log entry | observed outcome |
| function | rules of the game | dynamics, value function | deterministic program code | query, view, state machine | structural equation |
| choice | decision node | decision step | random choice | operation | treatment assignment |
| resolver | player, or Nature for chance | policy, environment | sampler, inference proposal | client, network | assignment mechanism |
| view | information set | observation | distribution and its arguments | snapshot | covariates |
| seal | end of the game | end of an episode | end of an execution | commit, watermark | end of follow-up |
| coupling | strategic interdependence | multi-agent interaction | dependency between random choices | contention | interference |
| goal | payoff | reward | inference objective | objective | estimand |
Two ideas carry over directly:
- Game theory’s information set, the set of situations a player cannot tell apart, is the counterpart of the view. A selection can be judged only against what its resolver could tell apart, so each record contains the view shown to its resolver.
- Probabilistic programming names each random choice by a stable address, so that an inference algorithm can change one choice, re-run the program, and reuse every other recorded value at the same address. This procedure is the counterfactual replay described under the goals principle.
Older work reached each principle, usually in one kind of system:
| Principle | Earlier form |
|---|---|
| Derivation | double-entry bookkeeping; derived state in Out of the Tar Pit (2006); event sourcing, which also stores external systems’ replies for replay; The Elm Architecture on one device |
| Binding | effect handlers; Daml, where only a choice’s controllers may exercise it |
| Sealing | Helland’s entities, each one scope of serializability |
| Prediction | tentative writes in Bayou, until a primary server commits them; Helland’s guesses and apologies |
| Effects | the output commit rule of log-based rollback recovery, which also logs every nondeterministic event, as derivation does |
| Grounding | grounding in communication between people; positions moved past concurrent edits in operational transformation |
| Coupling, Goals, Versions | the work cited in each section |
Open problems
- Inferring scopes. A compiler could read functions and invariants and report which choices need a sequencer, over which scope, and where escrow would remove the need. Indigo and Hamsaz perform this analysis for invariants written in restricted logics.
- Estimating coupling. Read and order coupling can be derived from functions and weighted from the records. No published method determines when a runtime may repartition a changing graph without invalidating experiments already running.
- Declaring response deadlines. Products do not record a response deadline per choice. Without one, the prediction principle cannot be applied mechanically.
- Specifications for AI agent resolvers. A choice bound to an agent needs a specification: what the view includes, which options exist, what budget applies, which results a person must confirm, and what must be recorded for replay.
- Stand-ins for people. Counterfactual replay past a person needs a stand-in. For averages over many runs, the g-formula states when models of each step suffice, but no accepted method validates a stand-in for one run.
- Sealing methods as mechanism design. The auction comparison shows that the sealing method changes when agents act. Frequent batch auctions, which seal an exchange’s orders in batches instead of one at a time, remove the reward for small speed advantages. A sequencer also determines whose record goes first, and no principle constrains that order when its operator has goals of its own. No catalog maps sealing methods to the behavior each one produces.
- Legibility of functions over a person’s records. Personalization and ranking compute what a person is shown from that person’s own records. Provenance can trace a view to the records it was computed from, but no method states which of those functions a view must present, or how a person can supersede the records they read, without the view becoming an audit log.
- A common unit of cost across resolvers. Guardrails can bound a person’s attention and a model’s tokens separately. A goal that trades one against the other needs a common unit, and no unit is accepted.
Toward a universal runtime for interactive software builds the theory as four runtime components: one for records, one for functions, one for choices and their resolvers, and one for seals. Toward a universal set of languages for interactive software designs a language whose structure follows the theory, so that a compiler can check the principles.