Shipping the Model: Prior Art for the Header Boundary Contract

A shared header was rebuilt six times against one oracle, and the artifact that survived was not any of the six implementations. It was a contract: a single reducer, patches that may only set fields their kind allows, adapters that contain no logic, and derived state that is recomputed rather than transported.

The obvious suspicion is that none of this is new, and that server and client frameworks have understood it for years. That suspicion is correct. What is worth writing down is which older idea each rule turns out to be, because each one comes with a known failure mode that the rule alone does not carry, and two of them would have prevented a defect that appeared three times in three substrates before anyone noticed it.

Related notes rather than repetition: the type-discipline reading of Racket contracts and Eiffel is in Type Systems for Software Developers; the UI invariant taxonomy is in Goldberry; the boundary taxonomy this note's last section returns to is in The Four-Boundary Spec Mapping.

Eight rules govern how state enters the header. Four of them are the interesting ones.

1. The header owns its own state machine. No patch may set menu_open,
   collapsed, focus_ring, aria or search_placement.
2. Field allow-list by kind. navigation may set route only.
4. Validate at the boundary, once. Every adapter runs the same validate().
7. Derived state is recomputed, never transported. active is never sent.
8. One reducer. Every adapter funnels into a single apply(patch).

And one invariant they buy:

For any set of adapters, and any interleaving of their messages, the rendered state equals fold(apply, initial, valid_patches_in_seq_order), independent of which transports delivered them.

Read that sentence again with the word fold in mind. It is the giveaway.

The reducer is a fold over actions. That is not an analogy, it is the naming: reduce applied to a stream of actions to accumulate one state. Redux's own prior-art documentation credits the lineage directly — it evolves Flux but takes its cues from Elm, and replaces Flux's dispatcher with pure functions because pure functions compose (“Prior Art –- Redux,” n.d.).

So rule 8 is settled prior art, and the header contract's version differs in exactly one respect worth noting: Redux reducers are pure but the store is singular by convention, whereas the header's reducer is singular by contract, because the alternative is eighteen transports each holding a private opinion about route. The rule is the same. The reason for it is stronger when the inputs are adversarial rather than merely numerous.

What Redux does not give you is the allow-list. A Redux action may carry any payload, and nothing structural prevents an action from setting derived state. That is rules 1, 2, and 7, and they come from somewhere else.

Design by Contract (Meyer 1992) fixes when an invariant must hold, and the answer is not "always". A class invariant must be satisfied whenever an instance is externally accessible: after creation, and after any call to an exported routine. It may be false during a routine's execution, provided it is restored before any other object can act on the receiver.

That is rule 1 and rule 4 together, and the correspondence is exact.

Eiffel's information hiding is why rule 1 can be stated at all. If a transport could set menu_open, the header would have two authorities over one field and the invariant would have no boundary at which to hold. The contract's phrasing — "the header owns its own state machine" — is a restatement of the oldest rule in the language.

Rule 7 falls out of the same place. active is a function of route and visible, so it is not state, it is a query over state. Sending it creates a second source of truth, and the failure mode is documented and dull: back and forward restore a route but not your derived value, and the two drift. Command-query separation says a query is computed, not stored, and the header contract says the same thing in transport vocabulary.

Racket monitors contracts on the flow of values across module boundaries, and the reason that placement works is the reason rule 4 works: checking once, at the point where responsibility changes hands, is both cheaper and more informative than checking everywhere.

The more useful borrowing is blame. Findler and Felleisen's contribution was not the checking, it was assigning responsibility for a failure to a specific party (Findler and Felleisen 2002). With first-order functions this is easy: a violated precondition is the caller's fault and a violated postcondition is the callee's. Higher-order arguments are what makes it hard, and what makes the formal treatment necessary. The subsequent slogan, that well-typed programs cannot be blamed (Wadler and Findler 2009), is the same idea sharpened.

The header contract already has a blame label and did not notice. Every HeaderPatch carries source, the adapter that produced it, and the reducer counts drops per source:

{ "v": 1, "seq": 42, "source": "actioncable", "kind": "domain",
  "patch": { "cart_count": 3 } }

That is blame assignment with the formalism removed. A rejected patch names the party at fault, which is precisely what an unblamed assertion cannot do. The gap between this and Racket's version is real but narrow: Racket's contracts compose, so a violation deep inside a higher-order value still names the right module, while the header's source is flat and only names the adapter that handed over the message. For eighteen adapters that are all first-order I/O, flat is sufficient. It would stop being sufficient the moment an adapter wrapped another adapter.

An adapter that contains no logic and funnels into one reducer is the shape algebraic effects give you by construction. Plotkin and Pretnar's handlers (Plotkin and Pretnar 2009) separate the description of an effect from its interpretation: an operation is a symbol in an algebraic theory, and a handler supplies a model for it. Two handlers, same program, different behaviour, and the program does not know which one it got.

Map it across:

This is also why the transport invariant is testable at all. "Replay the same patch sequence through different adapters and assert an identical DOM" is the statement that the interpretation is fixed and the delivery is not. In Haskell the same discipline is enforced by the effect library rather than by review: polysemy, effectful, and the older mtl all make the interpreter a value you pass in, so an effect described in one place can be run in another. The header contract achieves this by convention and a code review. An effect system achieves it by refusing to compile.

The most exact prior art for "validate at the boundary, once" is not Racket, it is Elm's port boundary. JavaScript is treated as untrusted infrastructure, so everything crossing into Elm is decoded, and the guarantee is that flags and ports cannot throw a runtime exception in your Elm application provided you type them as Json.Decode.Value and handle the failure case explicitly (“Protecting Boundaries between Elm and Javascript,” n.d.). The decoder is not optional politeness. It is the type system's price of admission.

This matters here because the same defect appeared three times in this project, in three substrates, and was silent every time.

Three occurrences, three languages, one shape: a key-representation mismatch at a JSON boundary, and never once an exception. In each case some validation existed and none of it was at the boundary. Elm's design makes this failure unrepresentable, not unlikely, and it does so by putting the check exactly where rule 4 says to put it.

The third row is the one to sit with. Seventeen of twenty-three acceptance tests passed against a header whose every label was the empty string, because structure survives an empty string and only the test that reads the text noticed. A boundary decoder would have failed at load. An acceptance suite mostly did not.

Strip out everything with a name and something small remains.

The corpus already identified it as the open problem. The four-boundary mapping puts message, composition, and interop boundaries in well-tooled cells and leaves the render boundary empty, with this diagnosis: the nearest formal frame is model-based UI testing, project a state machine and check the UI against it, "which is niche precisely because almost no UI ships the model."

Model-based UI testing is not missing. XState ships it: @xstate/graph computes paths through a machine with getShortestPaths, and the model-based testing utilities that used to live in @xstate/test were folded into that package in v5 (“Graph and Paths –- Stately / Xstate,” n.d.). The lineage runs back to statecharts (Harel 1987), and the Goldberry related-work note already places both.

The gap is the one the mapping named: the model is not a shippable artifact. In XState the machine is the implementation, so a test generated from it cannot disagree with it — the same reason a checker that restates the rule it checks is a copy rather than an instrument. The model and the code have one author, so agreement is guaranteed and therefore uninformative.

What the header work adds is narrow and, as far as the corpus goes, new: the model is exported from a core written in a different language than the UI. A sealed implementation enumerates its own reachable state space offline and publishes a labelled transition system — 51 states, 1071 transitions, from an Emacs Lisp core that cannot run in a browser. A ClojureScript renderer with no header logic walks it. The browser acceptance suite passes 23 of 23 against a header whose every decision was made ahead of time, by Emacs.

That inverts the usual dependency. The model is not a description of the UI maintained alongside it; the UI is a rendering function applied to a model that six independent implementations already agreed on, against an oracle none of them wrote. A renderer that contains no logic cannot disagree with the core it renders, which is the same property that made the model checker worth running, arrived at from the other direction.

Two consequences, one good and one limiting. The good one: a core in any language reaches a browser without being ported, and a trace from production replays against it in milliseconds with no browser. The limiting one: the export is finite, so it covers only an enumerable state space. Widths are handled by having the core probe itself and publish the partition it observes rather than letting the renderer assume a breakpoint. An unbounded input — a cart count, a signed-in name — has no such trick, and needs a live boundary instead.

Four instruments now grade this header, and the honest summary is that each one is blind to something another catches.

The model check's blind spot is structural rather than incidental, and it is the one worth stating plainly. A state carries no route, so no property written over states can relate a route to the item it activates — which is exactly the defect that made the first spoke score 2 of 25, with /researchx lighting up "Research". The calibration run exports a deliberately naive core every time and asserts that the checker still accepts it. A blind spot that moves without anyone noticing is worse than one that stays put.

None of the four says anything about whether the header looks right.

For the type-discipline reading of the same sources, including Racket's flat versus higher-order contracts and where Eiffel's contracts came from, see Type Systems for Software Developers: One Tool, Four Ways. For the taxonomy of what a render-conformance suite would need to check, see Goldberry. For where this boundary sits among the other three, see The Four-Boundary Spec Mapping.