Eight Implementations, One Spec: Redundancy as an Epistemic Device

The claim

lazily is a reactive library implemented in eight languages ... Rust, Zig, C++, Go, Dart, Kotlin, Python, JavaScript ... against a shared normative spec, with a Lean model behind the invariants and a load-test harness in front of them.

The claim this piece defends:

Multiple implementations are an epistemic device, not just a distribution strategy. The redundancy is the point. A design decision that is invisible inside one language becomes an argument between bindings, and the argument surfaces things no amount of care inside a single implementation would have.

The falsifiable version: if this were only about reach, the spec would be a description of the reference implementation and the other seven would be ports. It is not, and they are not. The spec has repeatedly been changed by the ports, against the reference implementation's existing behavior.

That is the thesis. The rest of this piece is what the method actually found, organized around the ideas rather than the order they arrived in ... including the places where the method misled, because a tool you cannot see mislead you is a tool you cannot trust.

A language can refuse to let an assumption stay unasked

The most direct payout of redundancy is adversarial: each language brings its own hostility to some assumption, and eight of them together interrogate a design from angles no author would think to choose.

Iteration order

Go deliberately randomizes map iteration order. So the Go binding's observers fired in a fresh order on every publish.

Every other binding had some order, stable enough that nobody had asked whether it was guaranteed. Go's runtime refused to let the question stay unasked. The answer the spec settled on ... firing order is registration order ... is now a MUST, with the reasoning that the alternative is not "some other order" but a different order per notification, and callers write observers with order-dependent side effects whether or not the contract admits it.

Deduplication

Two bindings deduplicated observers by callback identity: Python by equality via a set, Zig by address. Both are natural in their language. Neither survives contact with the family.

Deduplication is inexpressible where callbacks are neither hashable nor comparable, which is most bindings' natural closure type. But the portability argument turned out to be the weaker one. The real problem:

Two components that happen to subscribe the same bound method share one registration. The first to unsubscribe silently cancels the second's subscription. Neither component can see the other to defend against it.

That is ordinary code, not a hypothetical. An identity-keyed collection makes it the default behavior rather than a bug someone chose ... which is why the spec clause ended up a MUST NOT on the mechanism, not only on the effect. The bug was found by asking "how would Dart express this", not by finding the bug.

Allocation failure as an ordinary return value

The strongest instance of the pattern, because the failures it exposed are not divergences between bindings. They are unrecoverable.

Zig makes every allocation fallible and forces the call site to say something about failure. The convenient thing to say is nothing: catch {} on a push, catch return on an append. Eight such sites in the Zig binding, each written by someone reasonable, each with an implicit argument behind it ... this registration is best-effort; dropping one is a missed optimization at worst.

Every one of them was wrong, and wrong in the same direction. The clearest:

A dropped dependency edge does not cost one invalidation. The reverse-edge set is the only state any re-enqueue decision reads, and a slot's edges are cleared before every recompute ... so the slot never recomputes on that dependency again, and the recompute that would have rebuilt the edge is exactly the one that can no longer be triggered.

Silent, permanent staleness from a single swallowed error return. The same argument re-ran at each site with different nouns: a dropped cascade push stranded an entire subgraph serving values derived from a dependency that had changed; a dropped orphan-registration left a slot owned by neither the cache nor the orphan list, then went on to publish a fresh slot and return a correct value, so the operation reported success while leaking; a dropped invalidation seed left the slot itself marked fresh, not merely its dependents.

The fixes split two ways, which is the part worth keeping. Where a bound is known at construction time, reserve capacity up front so failure is reportable at a point the caller can act on. Where it is not ... a slot's edge count is unbounded and unknown when the slot is created ... propagate the error, or degrade to a conservative fallback that marks everything stale. Both are more work than catch {}. Neither is available to a call site that has already decided failure is uninteresting.

No other binding in the family can pose this question. The garbage-collected five cannot fail to register an edge for lack of memory in any way their code can observe. Rust aborts. C++ throws. Only the binding that makes allocation failure an ordinary return value forces someone to write down what the graph should do when it cannot afford to remember an edge ... and the honest answer turned out to be "anything except carry on silently."

The same sweep turned up two memory-safety bugs that were reported by an earlier audit and deliberately left because fixing them meant touching disposal: a use-after-free on a slot destroyed while queued for recompute, and a double-free from a payload destructor re-entering teardown on a reentrant mutex. Both are reachable from safe user code. Both are fixed, and each of the eight allocation-path fixes landed with a neutralization test ... restore the catch {} and the test goes red.

The primitive that six clauses could not save

This is the family's central result, and the shape of it matters more than the conclusion. The observer clauses in the specification were not a contract being refined. They were a mechanism failing in slow motion, one clause at a time, and the specification's final state on the subject is a prohibition.

The sequence, because the sequence is the point:

Four bindings independently grew a Cell.subscribe. Nobody coordinated it. The need was real.
Four bindings answered its open questions differently. Firing order, duplicate registration, reentrancy ... the same caller code behaved differently on different bindings.
The disagreements were resolved by writing clauses. Firing order is registration order. No deduplication by identity or equality. Subscribe-during-notify is deferred. Unsubscribe-during-notify is immediate. Disposers latch. Delivery is per write and unbatched.
Six clauses in, the bindings still disagreed ... and the specification itself was wrong twice along the way: it omitted a violated clause in one binding, and rested its central argument on two bindings that had never implemented the mechanism at all.
The sixth clause contradicted the surrounding model. "Delivery is per write, and batch does not coalesce it" put the mechanism in permanent conflict with the batching semantics every other primitive honours. That was the clause that could not be written without admitting the thing did not belong.
The specification now bans it. No reactive exposes an observer API ... not Cell, not Slot, not Signal. A binding conforms by not having one.

A primitive that needs six normative clauses to be safe, still diverges across the family after all six, and whose final clause contradicts the model it sits inside, is not under-specified. It is misdesigned. The clauses were never converging on a contract; they were an increasingly precise description of something that should not have existed.

The clause that looked like the strongest evidence

The clearest of the six deserves its own telling, because for a while it was the best argument this family had for the whole multi-implementation method ... and what it actually demonstrates is subtler.

Question: an observer is disposed from inside a notification callback. Does it still get invoked in the pass already in flight?

Five bindings said yes, implicitly, by taking a stable snapshot of the observer list before the first callback and iterating it. That is the simpler implementation, and under a tracing collector the extra call is harmless ... the closure is still alive precisely because the snapshot references it.

It is not harmless anywhere else. In a manually-managed binding, unsubscribe is routinely the step immediately before freeing the state the callback reads. "One more call after you asked to stop" is a use-after-free with a specification behind it.

The resolution:

A contract that is safe in five bindings and unsound in three is the wrong family default.

So the GC'd bindings migrated, rather than Zig, C++, and Rust adopting a rule they cannot honour. The majority lost. A JavaScript-only reactive library never has this conversation ... not because its authors are careless, but because nothing in the environment poses the question.

Every fact in that story held up. The GC'd behavior really was unsound for manually-managed bindings, the migration really did happen, and the reasoning about use-after-free is correct. And it was all in service of a mechanism that has since been deleted outright.

That is worth dwelling on, because it is a failure mode of the method this piece is arguing for. Eight implementations disagreeing said loudly that something was wrong, and said nothing about what. I read the disagreement as "this contract is under-specified" and specified it more carefully, six clauses deep, when the signal actually meant "this primitive is the wrong shape." Cross-implementation disagreement is a good detector and a bad diagnostician. It points at a region, not a cause, and the natural response ... write a clause ... is exactly the wrong move when the region contains a design error rather than an ambiguity.

Why an observer cannot be patched: coalescence

What made it a ban rather than a seventh clause were two costs that only became visible once the semantics were pinned down. The first is a correctness argument that no amount of specification can fix.

Coalescence deserves the emphasis, because in a lazy reactive graph it is not one mechanism but five, and together they are most of the point. An equality guard on writes drops a write that changes nothing. A memo guard drops a recompute whose result is unchanged, so downstream never learns. A batch folds many writes into one invalidation and one flush. Store-without-cascade skips effect scheduling entirely for a subgraph that has no effects in it. And the merge algebra folds a whole run of operations into a single state. Every one of those is the graph deciding that some change does not need to propagate ... which is exactly why a lazy graph is cheaper than recomputing everything, and a much larger share of the design than "batching" alone suggests.

The merge case is where this stops being an optimization detail and becomes a correctness argument, so it is worth being concrete.

Associativity is the irreducible law of a merge policy, and what it buys is variable flush points: a bounded relay may flush at any post-merge watermark and converge to the same state. The converged state is guaranteed. The sequence of intermediate values is not. Two runs of the same program over the same operations can legitimately produce different intermediate values under different backpressure, buffer sizes, or transports.

An effect reads the converged state ... the value the algebra actually promises. An observer fires on the intermediates, so what it receives is an artifact of flush timing rather than data, and it is non-deterministic by design rather than by defect. There is no contract there for a caller to write correct code against.

Last-writer-wins sharpens it to a point. The keep-latest policy is old ⊕ op = op ... the new operation annihilates the previous state ... and a plain cell is the keep-latest instance, so every cell in the system is already an LWW register. Under a timestamped LWW register, a losing write is dropped outright: after convergence, it never happened. An observer that fired on that write reported an event the system has since decided did not occur ... and whatever side effect it took, a log line, a queue push, a paint, an outbound message, now describes a state that no replica will ever agree existed. An effect never sees it, because it observes only what survived the merge.

Which is the entire objection at its most concrete: observers report writes; the system's semantics are about values that survive. Those are different questions, and in a coalescing, converging, distributed graph they diverge constantly.

An effect sits downstream of the coalescing machinery. It sees what the graph decided was worth propagating. That is why it can be glitch-free, and why writing to a subgraph nobody is watching costs nothing.

An observer sits upstream of it, and outside all of it. It fires on the raw write, before coalescence has a chance to apply. So it receives a flat sequence of callbacks with no framing: three invocations might be three separate updates or one grouped update, and nothing distinguishes them. It cannot see what was elided either ... a write the equality guard dropped, a recompute the memo guard suppressed, a flush that never happened. "The value did not change," "nothing was written," and "the graph decided this did not need propagating" are all the same non-event.

It is an event stream stripped of both its transaction boundaries and its elisions. And that is not a missing feature to be added; it follows from sitting outside the graph. The graph is the thing that knows where an update starts, where it stops, and what it chose not to do. A callback list hanging off one node is structurally unable to observe any of it. An effect gets all three for free, because running once per settled cone is the boundary.

So a caller holding an observer is looking at a system whose central optimization is invisible to them ... unable to tell a change that mattered from one the graph deliberately suppressed. Two mechanisms, and only one of them can express "this update is complete."

Isn't a reactive just an observer with extra steps?

The two look interchangeable at the call site. They are not, and it is worth being blunt about where they differ:

	Effect	Observer
Registration	implicit ... reading a value declares the edge	explicit ... hand over a callback
Position	a node in the graph	a list hanging off a node
Runs	once per settled cone	once per write
Batch	honours it	ignores it
Coalescence	sees the coalesced result	cannot see what was suppressed
Glitch-free	yes	no ... fires mid-update by construction
Dependencies	dynamic, re-discovered each run	none, bound to one node forever
Teardown	disposed with its scope	manual, outlives its scope
Cost when unused	zero	storage on every node

A reactive graph observes by declaring an edge. You read a cell inside a computation; the tracking stack records the dependency; invalidation propagates structurally; the graph decides when dependents run. Nobody registers a callback. Every guarantee the system makes ... batching, glitch-freedom, coalescing, cone-settled consistency, scope teardown ... follows from the graph knowing what depends on what.

Cell.subscribe is a callback list stapled to a cell. It knows none of that. It cannot batch, having no notion of a cone to settle. It cannot be glitch-free; it fires mid-update by construction. It is not a node, so it does not participate in teardown. It is the observer pattern, living inside the reactive primitive and bypassing it.

Which makes the standing objection to reactive systems ... isn't this just an observer with extra steps? ... locally, literally true. Not as a rhetorical gotcha. There was an observer registry inside the cell and callers could reach it. The honest answer to the question is that a reactive is not an observer, and the way to be able to say that is to not ship one.

The memory bill

The second cost was carried by the graph itself. Observer storage sits on every node whether or not anything registers. Removing it from the Zig binding moved sizeof(Cell) from 168 bytes to 32 ... 136 bytes off every cell in every program, an 81% reduction. Roughly 112 of those bytes were inline edge sets; the rest were reentrancy counters and a registration counter, unconditional per-node state existing solely to make the notify loop safe. A reactive graph's entire value proposition is holding many nodes cheaply. A per-node cost multiplied across the graph is the one kind of overhead it cannot absorb, and this one was being paid by every reactive value in the system to support a feature with exactly one caller family-wide (state machines) and one legitimate use case (needing every transition rather than the settled one).

And the semantics that the six clauses were pinning down were footguns, not bugs. Every failure lived at an edge: delivery ignoring batch while everything beside it honours batch; firing order depending on a hash table's rehash; two components subscribing the same bound method, silently sharing one registration, so the first to unsubscribe cancels the second; a disposer removing a later caller's registration; one more invocation after asking to stop ... harmless under a tracing collector, a use-after-free without one. Each is fine in the common case and wrong in a case the caller cannot see coming. Correct code and broken code look identical at the call site. That is the definition of a footgun, and it is not fixable by documenting it harder.

A Topic hiding inside a Cell

The one legitimate use case has a home already. A Cell is a value: latest-wins, batched, glitch-free. A stream of every transition is a different thing, and the family has had it the whole time ... Topic, in all eight bindings, with cursors and durability. Topic.subscribe keeps its name, because a topic genuinely is a subscription: an ordered stream read at the consumer's own position.

So the defect had a shape after all: a Topic hiding inside a Cell. Four bindings grew one because the need was real and the nearest surface was the wrong one. Naming it wrongly is what let it sit there ... which is the second time this family has found an architecture bug underneath a naming ambiguity, after Signal was demoted from core primitive to derived construct for the same reason.

The outcome: Cell observers are a MUST NOT in the spec, the six observer_* fixtures are deleted, and the four bindings that grew the API are removing it and re-expressing on_transition as an effect. A binding conforms by not having it.

What this cost: the four observer migrations described above ... the careful registration-keying work, the liveness fixes, the token API ... are deleted by the ban. They found the problem. They do not survive it. I would rather record that than pretend the path to the conclusion was a straight line.

A family can manufacture consensus

The most uncomfortable finding, and the least resolved.

The disposal story above is stated in the spec as a count ... safe in five bindings, unsound in three ... and names the three. On auditing the family for conformance, two of those three named bindings turn out to have no observer API at all. Neither does a third binding elsewhere in the family. Their Cell type has no subscribe, no on_change, no listener collection; the only subscribe present is an unrelated queue cursor. They express observation through effects and dependency edges instead.

One of the two is the reference implementation.

So the five-three split is not a description of this family. Of the bindings cited as unable to honour the rule, exactly one implements the surface the rule governs. Three other bindings had already migrated against that reasoning.

I do not think this makes the decision wrong. The one binding's hazard is real, and any future manually-managed implementation would hit it identically. But the argument now rests on one implementation plus a claim about hypothetical ones, which is a materially weaker thing than what the document says, and the difference was invisible for as long as nobody checked which bindings actually had the API.

There is a nastier reading available, and honesty requires stating it: a multi-language family can manufacture the appearance of cross-implementation consensus about a feature that most of its implementations do not have. The redundancy that makes disagreement informative also makes it easy to count bindings that were never in the conversation.

This remains unresolved, deliberately. Either the clause survives on the narrower justification or it does not, and that is a decision, not a finding.

A conformance suite is an implementation too

The counterweight to everything above, and the reason this piece is not a victory lap: the machinery built to keep eight implementations honest turned out to have every failure mode it was built to catch.

The spec ships conformance fixtures as JSON. Thirteen of them cover the reactive graph ... observer semantics, disposal, teardown scopes. On inspection: no binding executed any of them. Not one, in any of the ten repos. The family had converged on hand-transcribing fixture semantics into each language's test suite instead of loading the JSON. Transcriptions drift.

Writing real fixture runners produced the finding that actually matters:

The spec's own table of known divergences was incomplete. It recorded two violated clauses for the Python binding. There were three. Python also invoked observers that had been disposed mid-notification ... the same defect the table carefully documented against two other bindings, in the same table, in the same revision. It went unrecorded because a Python test pinned the behavior as intended and the docstring described it as a deliberate "snapshot dispatch" design.

That is the whole thesis inverted and pointed at itself. A hand-maintained audit of where implementations diverge from a spec is itself an implementation of the spec, and it drifts the same way. The fixtures found it in one run. Reading the table did not, and I had been reading the table.

Three ways to be green while testing nothing

The obvious hypothesis for how the divergence survived ... CI skipping the fixtures ... turned out to be wrong, and wrong in an instructive direction. The CI did check out the canonical spec. The actual mechanism is worse:

Several bindings resolve fixtures local-first ... a bundled copy under the test tree, falling back to the canonical sibling only when the copy is missing. So CI faithfully checks out the source of truth and then shadows it with a stale duplicate. One such copy had already diverged from its source by a third of its size. Nothing skipped. Nothing warned. It was green the entire time, and a skip-if-absent guard cannot detect it, because nothing is ever absent.

And a third binding exhibited a third mechanism, worse than both: its CI never cloned the spec at all. Every conformance test in that repo ... not the observer ones, all of them, across a dozen fixture areas ... had been skipping silently in CI since the day they were written. Green the whole time. Executing nothing.

Three bindings, three different ways to report success while testing nothing:

Mechanism	What CI sees	Caught by an absence guard?
Spec never cloned	Every suite skips, silently	Yes ... this is the case guards are for
Cloned, but local copy resolved first	Stale duplicate runs, passes	No. Nothing is absent
Copy bundled into the repo	Drifted duplicate runs, passes	No. Nothing is absent

Only the first is the failure mode I had assumed, and the fix I initially propagated ... skip-if-absent guards ... addresses only it. The other two are the majority, and they are immune to it. Which is its own small lesson about fixing a bug class from one instance.

A fixture that does not run is worse than a missing fixture. But the dangerous case is not the one that skips loudly ... it is the one that runs something, passes, and names itself after the thing it is not checking. Resolution order is a correctness property.

There is a structural point underneath all three. Every one of these is a conformance suite that cannot fail, and none of them was detectable by reading the suite ... they all look correct, and their names all describe work they were not doing. The only thing that surfaced any of them was running the fixtures and checking that a known-divergent binding actually went red. Which means the red-first discipline was not a testing nicety here. It was the sole instrument that could distinguish a passing suite from an empty one.

The repair ran family-wide. Final tally: every binding except the Rust reference could report a green conformance suite while executing nothing. And two of my own claims fell on the way through, both to measurement rather than reasoning:

The drift I kept citing as the motivating example had already been fixed by an earlier session. At HEAD, all 87 Kotlin fixtures and all 33 C++ vendored fixtures were byte-identical to canonical. I had been repeating a stale fact because it was written down and I never re-checked it.
Kotlin's real defect was not drift at all but coverage: nine fixtures sat behind silent if (!present) return guards, in spec areas it had never bundled, asserting nothing for their entire existence. A byte-comparison script ran in CI the whole time and was structurally blind to it, because it only compares fixtures that are bundled. The check was real, passing, and incapable of seeing the problem.

That last one is the sharpest version of the whole section. The defense against drift was itself a thing that could pass while not looking.

The fourth way: a corpus that cannot fail

With delivery repaired, all eight bindings replay the reactive-graph corpus, most of them against all three execution contexts rather than only the synchronous one. That closed the coverage hole and immediately exposed a fourth failure mode, one that survives all three fixes above.

lazily-dart and lazily-cpp independently mutation-tested their disposal implementations against the nine-fixture disposal corpus. Two bindings, two sessions, no coordination, same result:

Mutation applied to the implementation	Corpus verdict
Remove the dirty-cone cascade	red, 3 divergences per context
Schedule effects during disposal	9 of 9 green
Run teardown forward instead of reverse	9 of 9 green

So every binding reporting nine-of-nine was conforming to a corpus that pinned one of the three semantics it is named after. The fixtures ran. They resolved from canonical. They were byte-identical to the source of truth. They asserted almost nothing.

The reason is mundane once you see it, which is exactly the problem. Every existing fixture disposed the effect that sat inside the cone, so the corpus never once had a survivor available to spuriously schedule. And the single fixture carrying a cleanup_order assertion owned exactly one effect ... a one-element log reads identically forwards and backwards. Neither gap is visible by reading the fixture. Both are visible in one mutation run.

Mechanism	What CI sees	Caught by
Spec never cloned	every suite skips, silently	an absence guard
Local copy resolved first	stale duplicate runs, passes	a resolution-order audit
Copy bundled into the repo	drifted duplicate runs, passes	byte-comparison against canonical
Corpus runs and cannot fail	genuine fixtures, genuinely passing	mutation, and nothing else

Which restates the lesson one level further up, and I think this version is terminal:

A fixture that does not run is worse than a missing fixture. A fixture that runs and cannot fail is worse than both, because every instrument you built for the first two reports it as healthy.

Two new fixtures close the two gaps: one leaves a live effect downstream of the disposed node, one gives a scope three effects instead of one.

The fifth way: a capability that was only a type name

The same audit asked a different question ... not "does this binding run the fixtures" but "does this binding implement the thing the fixtures are named after." Shipping a type called AsyncContext is not the same as having one.

One binding's async context had no dependency graph at all: its async slot node carried neither dependents nor dependencies, its async read recomputed unconditionally on every call, and its synchronous read returned a cached value that nothing ever invalidated. Depth tests passed because nothing was memoized. An implementation that never caches cannot serve a stale cached value, so a corpus asking "is the write visible at depth" is satisfied by an implementation that does no work at all.

The spec now records capability status as measured, per binding, with unmeasured written out where nobody has looked ... rather than inferred from the presence of a type name. Two bindings that both ship a ThreadSafeContext turned out to mean materially different things by it: one shares a mutex across worker realms while each realm keeps its own graph, the other is a single-isolate reentrancy guard. Both are honest in their own sources. Neither is the shared-graph guarantee the shared name implies.

The unmeasured cells are deliberate, and they are the same lesson as the divergence table: absence of a finding is not a finding. Three bindings' omission from that table meant nobody had looked, and it read for months as though they conformed.

Where this leaves the suite: delivery closed, coverage closed, adequacy newly open. Every binding replays the corpus; the corpus is now known to under-specify at least one area it covers, and mutation is the only thing that told us.

What one implementation, read beside another, can find

Everything above is arguing that multiple implementations are an epistemic device. Here is the clearest instance, and it happened by accident.

An agent building an async context for the Python binding read the Dart binding as a reference ... Dart being garbage-collected and object-shaped, so a closer model than Rust. While reading, it noticed Dart's invalidation didn't match Rust's: Dart registered slot-to-slot dependency edges but only ever fired invalidation from a cell write. Rust walked the whole transitive frontier.

That mismatch was a real bug. In a chain cell → a → b, writing the cell invalidated a, and b served a stale cached value forever. An audit then found the identical defect in the Go binding. Both are now fixed.

Neither binding's own test suite could have caught it. Not "didn't" ... couldn't. Every async slot test in both repos reads a cell directly; nothing anywhere composed a slot on top of a slot. The defect was unreachable from the tests that existed, in both languages, independently.

What found it was one implementation being read beside another.

And the failure has a precise shape, which is the part worth keeping. Two strategies for making a write visible at depth are both correct:

Eager marking ... the write walks the dependent cone; reads trust the flag.
Lazy pull ... the write marks little; every read refreshes its dependencies recursively before deciding whether to recompute.

Both bindings had built a hybrid: mark one level eagerly, and let reads short-circuit on a node that looks clean. Each half is defensible in isolation. Together they lose writes at depth two, because the mark never arrives and the read never looks past it. That is why it survived review ... there is no line of code that is wrong on its own.

It's now a theorem in the Lean model rather than a war story: hybrid_serves_stale_value_at_depth_two, three nodes, decide-checked, and a spec fixture at depth four.

The uncomfortable epilogue. A fixture that would have caught this already existed in the shared spec ... a depth-2 chain asserting the sink refreshes after a source write. It had existed for some time. When the bug was found, only one binding of eight replayed that corpus.

So the family had: a correct specification, a fixture encoding the exact property, two implementations violating it, and no mechanism connecting them. Which is the conformance-suite finding one level up ... repairing how fixtures reach a binding is worthless while bindings run none of them. That gap is now closed: all eight bindings replay the reactive-graph corpus, most against all three contexts, with CI deriving the expected replay count rather than hardcoding it. What replaced it at the top of the worry list is the adequacy problem: the corpus they all now run is known to under-specify at least one area it covers.

Three bindings, one wrong idea, one fixture

If the thesis is right — that redundancy is an epistemic device — then somewhere there should be a case where several implementations independently make the same mistake, and a single shared assertion catches all of them at once. Here it is, and it is cleaner than the observer arc that this piece was originally built around.

The setup is a specification failure of a kind not yet described here. The spec defined the derived Signal construct twice, in detail, in two separate sections: a memo slot plus a puller effect, materialized by the time the invalidating write returns, disposal reverting it to lazy. Good prose. It contained no MUST, no SHOULD, and no fixture. It was a description wearing a specification's clothes, and it had been that way for months.

Making it normative meant asking what a caller can actually observe. That question has an uncomfortable answer: an eager signal and a lazy memo return identical values for every read sequence. Eagerness changes when compute runs, never what a reader sees. So every assertion in the corpus — all of which compared values — was structurally incapable of telling signal() from memo(). Pinning the contract required a new observable: a cumulative count of how many times each compute had actually run.

With that in hand, one clause did the work:

Inside a batch, a signal whose dependencies are written N times MUST re-materialize once, at the outermost batch exit — not once per write.

A composed signal satisfies this for free: the puller is an ordinary effect, effects are scheduled rather than inline, so N invalidations coalesce into one run at the flush. A signal that re-pulls from an invalidation handler cannot, because invalidation is earlier than the flush.

Four bindings failed it, by two unrelated routes.

Three of them — Python, Dart, and Go — had independently grown the same signal-specific slot subclass whose invalidation handler re-pulls inline, with no effect anywhere in the construction. Three languages, three authors, no coordination, one wrong idea. The fourth, Zig, had a correctly composed signal and failed anyway: its set_cell flushed unconditionally while batch merely nested a depth counter. A composition is not sufficient if the batch boundary does not gate the flush.

Every one of them returned correct values. Two computes where the contract says one; five where it says three. That is why the defect survived eleven other fixtures in the same area, a Lean model, a load-test harness, and every code review anyone gave it. It is not a wrong answer, it is the same answer arrived at two to three times as expensively, and nothing in the system was looking at cost.

Two things about this are worth more than the bug count.

The formal model went first, and that turned out to matter. The theorems were written before the measurement, from the spec rather than from any implementation, and they proved not just that a batch of N produces one compute but that N unbatched writes produce N. Having both numbers meant a failing binding could be diagnosed rather than merely detected — a count that scales with writes is a per-write puller, a count that scales with distinct sources is a per-source one, and a count of N when batching should apply means the batch boundary is not doing anything. The model supplied the shape of each failure before any of them were seen. That is the first time in this project that formal methods did something the ports and the load tests could not, and I have spent this entire piece noting the opposite.

And I made the specification's own characteristic error while writing it. In the same pass I wrote a MUST NOT forbidding bindings from exposing the signal as a distinct node kind. It survived a few hours. A binding maintainer pointed out that in a language where the node base class is private, that property is not something a caller can observe at all — so the clause mandated an unobservable representation, which is precisely what this specification refuses to do everywhere else, and refuses for a documented reason. It is now a SHOULD NOT with the reasoning written out. I had been enforcing that rule against other people's bindings for a month and broke it myself inside an hour of picking up the pen.

The last binding is the one that did not get fixed, and it is the most interesting. Go's failure is not the welded signal — that was repaired. It is that Go's cascade consumes reverse edges as it walks. Moving the memo's equality guard to pull time requires marking a dependent clean without recomputing it, but a dependent that does not recompute never re-registers its edge, so its source can no longer reach it and the next genuine write is lost at depth two. Which is hybrid_serves_stale_value_at_depth_two, the theorem from earlier in this piece, arrived at from a completely different direction.

So the honest outcome for that binding is a recorded divergence rather than a fix. Repairing it means migrating both of its propagation engines to a non-consuming mark-frontier walk, re-deriving thirty degree assertions calibrated to the old behavior, and splitting a boolean that currently conflates "no value" with "dirty" across sixty call sites. There is a shortcut that would make all four clauses pass without touching propagation — defer the guard to flush time and un-mark using the existing edge-repair layer — and it is exactly a third variant of one-level-marking-plus-repair, the family the theorem is about. It would satisfy every fixture while diverging from the model. Declining it is the whole discipline in one decision.

A clause with a seam in it

A small finding, and a good miniature of how a specification fails without being wrong.

Two documents said complementary things about effect cleanup. One specified the ordering: cleanup completes before the next body starts. The other specified the trigger: cleanup runs before each rerun and on dispose. Each clause is correct. Neither is wrong in isolation. Together they left enough rope for one binding to run cleanup at the end of every flush whenever no rerun was queued ... which satisfies the ordering clause vacuously, because there is no next body to be ordered against.

The consequence is not academic. The canonical effect acquires a resource in the body and releases it in the cleanup. Running cleanup at flush end releases while the effect is still live and will rerun later, so an effect that subscribes and returns an unsubscribe unsubscribes itself immediately.

Two things about how it was found:

It surfaced only once that binding built a reactive-graph runner. Its synchronous surface had always been correct, so no test in the repo covered the difference. The corpus-replay work is what made it reachable.
The fixture that caught it asserts an empty cleanup log at a step where nothing is disposed and nothing is invalidated. An assertion that something did not happen. Every other fixture in the area asserts presence, and none of them could see a cleanup that fired when it should not have.

The trigger is now normative rather than the ordering, and two other bindings already behaved that way ... so this records the family's behavior rather than changing it. The outlier was the one that had read both clauses and satisfied both. A clause split across two documents is a clause with a seam in it.

Numbers that deserved suspicion

Chasing an O(n²) dependency-edge defect with a load test found four more defects, which is the happy version of the benchmarking story.

The unhappy version: on a shared workstation, the same benchmark row measured 336 µs, 435 µs, and 208 µs across three runs of identical code. A fan-out row swung 1.6x across four runs. Any conclusion drawn from a single run of that harness on that machine was noise wearing a number's clothes. Timing-sensitive work moved to a dedicated host, and the results that depend on it are blocked rather than estimated ... the huge-pages follow-up waits on hardware.

A related result worth recording, since it is the kind of thing a family makes visible: the crossover threshold where the edge-index optimization pays for itself differs per binding ... 32, 64, 128, 160 across four of them. There is no family constant, and picking one would have been a plausible, wrong, unfalsifiable decision. The corollary we keep re-learning: measure the hybrid, not the pure crossover.

The same discipline gates the comparison that has not been run yet. rmemo is the cleanest natural experiment available: same primitive, opposite propagation policy. Its set drains eagerly by level; lazily marks dirty and recomputes on read. The hypothesis it would test ... eagerness is a scheduling policy, not a data structure ... is stated elsewhere and not yet measured here, deliberately. Measuring now would compare a finished implementation against a half-finished one, which produces a number that looks like evidence and is not. It waits until the optimization work lands.

What I am not claiming

Worth fencing off, because the thesis is easy to over-read:

Not that eight implementations are worth it for most libraries. The redundancy cost is enormous and most of it is not epistemic.
Not that the spec is correct because it is multi-language. The conformance section above is a spec that its own implementations violated, shipping fixtures that proved it and that nobody ran.
Not that formal methods caught these. The Lean model carries the behavioral invariants behind the fixtures, and it has been useful ... but every finding in this piece came from a port disagreeing, a load test, or reading code. That asymmetry deserves its own treatment once I understand it.
Not that cross-implementation disagreement diagnoses anything. It is a good detector and a bad diagnostician, and read wrongly it produces six careful clauses around a primitive that needed deleting.

Open threads

Mutation-verifying the rest of the corpus. Two bindings mutation-tested one area and found it pinned a third of what it claimed. Nothing says the other twenty areas are better. This is the largest open item.
Measuring the capability table's unmeasured cells, and deciding what to do about the binding whose async context has no dependency graph.
Auditing the divergence table itself against runner output rather than against reading. The conformance section says why.
Deciding whether the disposal clause survives on its narrower justification ... one real implementation plus hypothetical future ones ... now that the five-three count is known to be wrong.
Huge pages. Blocked on a dedicated host.
The rmemo comparison. Gated on the optimization work finishing.
The formal-methods asymmetry noted above ... which now has a counterexample pointing the other way and needs rewriting rather than resolving.
One binding's migration to a non-consuming cascade, scoped and deliberately not started on the night it was discovered. Its sync plane is being done; its async plane is scoped out and the divergence between them is now recorded rather than fixed.
Renaming the derived primitive. The name it currently carries collides, with three different meanings, in three of the ecosystems this family ships bindings into. Nobody audited it against those ecosystems before adopting it, which is the same shape as everything else in this piece.

What changed, and why

Several claims in this piece were falsified within hours of being written, and they failed the same way. Every one of them came from reading something already written down. Every correction came from measuring. The divergence table, the spec's own count of which bindings were unsound, the drift I kept citing as a motivating example, my own earlier draft ... all of them were text I trusted because it existed, and all of them were wrong in ways that one run would have exposed.

That is the conformance argument above, pointed back at its author. A hand-maintained record of what the implementations do is itself an implementation, and it drifts. I had been reading the table rather than running the fixtures, repeating a fact about Kotlin and C++ drift that an earlier session had already fixed, and asserting a five-three split between GC'd and manually-managed bindings without checking which bindings had the API the split was about. Two of the three named turned out not to have it. One of those two is the reference implementation.

The essay form hides this by construction. A running log shows its corrections because it accretes; an essay presents a settled view and has to decide to admit what moved. The largest reversal is the one that cuts against the thesis rather than for it. The disposal contract ... non-GC bindings overturning a rule the GC'd majority was happy with ... was the strongest evidence here for multi-implementation development, and it is now a story about a mechanism that does not exist. Every fact in it held. It was in service of six clauses accumulating around a primitive that needed deleting, and I read the disagreement as specify this more carefully when it meant this is the wrong shape. A detector that fires accurately and points nowhere in particular will absorb as much careful work as you are willing to give it.

One claim in this piece has since been overturned by measurement rather than merely corrected, and it is the one I was most confident about. I wrote that formal methods had not caught anything here — that the Lean model carried the invariants but every actual finding came from a port disagreeing, a load test, or reading code. Then the model was extended to cover the derived eager construct, written from the specification before any binding was measured, and it proved not only what a correct implementation does but what each kind of incorrect one looks like: a count that scales with writes, with distinct sources, or with nothing at all. All three shapes were subsequently found in real bindings, and having the shapes in advance is what let each failure be diagnosed instead of merely detected. The asymmetry I spent this piece describing is real and I no longer think it is permanent.

The same asymmetry runs the other way on timing. The largest open thread here ... seven of eight bindings replaying none of the fixtures ... was true when it was written down and false within hours, because writing it down is what got it fixed. What replaced it at the top of the list is worse than what it displaced: all eight bindings now run the corpus, and mutation testing says the corpus under-specifies at least one of the areas it is named after. Measuring closes things fast and tends to reveal that the thing you were worried about was the smaller problem.