The jump is evidence

Imagine a search box that stays still for a, as, and asd, then jumps when j arrives. Backspacing across f makes it jump again. The letters are not special. They cross a hidden boundary: perhaps an empty result group appears, a toolbar changes width, or one animation enters while another leaves.

A screenshot records the symptom. A component model names the cause. Let a component have state $S$, events $E$, effects $F$, and rendered observations $O$:

$$update:S\times E\to S\times F^*, \qquad view:S\to O.$$

The star means a finite sequence of requested effects. update decides; an interpreter performs. The separation matters because a generated event trace can now exercise every reachable prefix without a browser, while a browser journey can check the geometry, focus, motion, and timing of the same semantic path.

Match the symptom to the structure

This is not a claim that every interface problem has one favorite abstraction. A search component may use a machine for request ownership, a monoid for result counts, and a canonical form for query tokens. The useful question is narrower: which law would make this observed failure impossible?

One autocomplete, several proof obligations

An autocomplete might have these states:

closed
open(query, activeOption)
waiting(query, request)
showing(query, request, results, activeOption)
destroyed

The tagged alternatives prevent destroyed from accidentally retaining an active request. The transition table then forces questions callbacks usually evade: What does results-arrived mean after close? What does ArrowDown do when there are no options? Does destroy cancel a timer that has not fired?

The WAI-ARIA Authoring Practices combobox pattern adds observable keyboard and focus obligations. Those are not separate from the machine. They are predicates over its rendered projection: the focused option is reachable, its identifier names a present element, and closing the popup returns the ownership of focus to the input.

One semantic path, several witnesses

A pure trace and a browser journey answer different questions.

• The pure trace checks total transitions, invariants, deterministic replay, convergence, and round trips over many generated histories.
• The browser journey checks focus, accessible names, hit targets, geometry, motion, network behavior, and timing in a real rendering engine.
• A profiler is conditional evidence: capture it when a timing budget fails, then use it to locate work. It is not the pass/fail oracle.

The shared object is the semantic journey: open search, enter text, delete backward, move through results, choose one, close. Adapters may drive that journey through human input or a semantic control API. Their observable outcomes should agree even when their mechanics differ.

From chapter law to test shape

The reusable harness follows one recipe:

1. name the law, not the implementation branch;
2. generate values or bounded event traces from a recorded seed;
3. evaluate a pure oracle;
4. shrink a failure to the smallest witness;
5. retain that witness as a regression;
6. run the same suite under the ordinary test runner and the hermetic build gate.

For a state machine, test deterministic replay and an invariant after every reachable prefix. For a partial order, test reflexivity, antisymmetry, and transitivity. For a canonicalizer, test idempotence, soundness, and completeness. For a codec, test both round trips. The mathematical name supplies the finite checklist.

EG-walker is several chapters meeting in one editor

EG-walker, the collaborative text algorithm described by Joseph Gentle and Martin Kleppmann, is a strong transfer specimen. Its durable history is an event DAG rather than a single event list. Causally related edits are ordered; concurrent edits may be incomparable. During merge, a walker replays from a shared causal frontier and constructs the sequence-ordering machinery it needs transiently instead of retaining that machinery as the document's permanent state.

Several book ideas become one design:

• the event graph is Chapter 10's DAG and Chapter 20's partial order;
• replay is a fold, and its event sequence uses Chapter 11's composition law;
• the walker's current causal frontier is state: the future-relevant summary of the history already replayed;
• concurrent delivery schedules are metamorphic inputs—the final document must agree across every admitted topological ordering, duplication, and partition schedule;
• checkpoints are canonical summaries that bound replay without changing the observation;
• transport, storage, and peer discovery are effects interpreted outside the pure replay kernel.

So EG-walker is related, but it is not “just another state machine” or “just a CRDT law.” Its verification harness needs generated event DAGs, several legal topological schedules for each DAG, deterministic replay, a reference sequence oracle, checkpoint round trips, and adversarial synchronization schedules. The generic machine and partial-order kits cover pieces of that obligation; a dedicated event-graph adapter should compose them rather than hide the graph inside a one-off test.

Honest limits

A generated law is only as strong as its generator, equality, and observation boundary. An invariant can be true and useless. A bounded trace cannot prove eventual progress beyond its bound; it must report inconclusive rather than pass. Browser automation cannot replace manual assistive-technology evaluation, and a simulator cannot reproduce every device, keyboard, compositor, or accessibility setting.

The gain is still substantial: once a component states its state space and laws, whole families of illegal combinations, stale transitions, and order-dependent outcomes stop being mysterious callback bugs.

Lessons

• UI components combine several discrete structures; the visible widget is their observation boundary.
• Tagged states remove illegal combinations, and transition tables expose missing temporal cases.
• Algebraic laws turn regrouping, reordering, normalization, and replay into generated checks.
• Pure traces and browser journeys are complementary witnesses of one semantic path.

Practice

1. Take a tooltip with delayed opening. Name its states, timer owner, focus owner, and every event that may arrive after detachment.
2. For a result list, write one semantic invariant, one accessibility observation, and one geometry observation. Explain why none subsumes the others.
3. Find a component with three related Boolean flags. Replace the product of eight combinations with the reachable tagged alternatives.
4. One week later, diagnose a UI race without using the words “timing issue.” Name the state, event, owner, and missing transition instead.

References

1. Dijkstra. “On the Role of Scientific Thought.” EWD447, 1974. — precision through abstraction
2. W3C Web Accessibility Initiative. “Combobox Pattern.” ARIA Authoring Practices Guide, current. — focus and keyboard interaction obligations for comboboxes
3. Microsoft. “Actionability.” Playwright documentation, current. — browser-level visibility, stability, event-receiving, and enabled checks
4. Gentle and Kleppmann. “Collaborative Text Editing with Eg-walker: Better, Faster, Smaller.” arXiv, 2024. — event-graph replay for collaborative sequences