The Bug That Wouldn't Compile: Porting a Reordering Mistake to Hydro

Marc Brooker spent an April post — "It's time to be right." — arguing that what limits agentic software development is not model capability but the defect tail: the rare, severe mistakes, not the average output. His proposed direction is tooling that makes whole defect classes impossible to write, and he names two systems from that family: Cedar for authorization and Hydro for distributed systems.

I have read versions of the correct-by-construction pitch for years, usually attached to research prototypes I never got to hold. Hydro is different in one respect: it ships. The hydro_lang crate has been cutting 0.17 alpha releases through June 2026, and the repository carries the compiler tests to back its claims. So I ran the experiment the pitch implies. I took a small aggregation of the kind I have hand-rolled many times, planted the reordering bug that class of code always grows, reproduced the bug deterministically — and then ported it to Hydro to see exactly which line the type checker would refuse.

The short version: the bug did not survive the port. Not because Hydro found it, but because the buggy line needs an ordering assumption the types would not let me hold silently. The longer version is more interesting, because what Hydro guarantees and what it merely makes you sign for are different things, and the difference is where I would base an adoption decision.

A 600-message aggregation that answers 291

The setup is the smallest shape of a pattern I keep meeting: N workers each hold a local counter and periodically report (worker_id, cumulative_count) to an aggregator, which folds the reports into a global total. Cumulative reports are the textbook choice here — they self-heal after a lost message, since the next report carries the full value.

The hand-rolled aggregator applies each report with an assignment: state[worker] = value. That line embeds an invariant nobody wrote down: reports from one worker arrive in the order they were sent. On a single TCP connection that holds. Add a retry path, a second hop, a load balancer, or a UDP transport, and it quietly stops holding.

Here is the whole experiment in one file — the sender order, a deterministic reorder standing in for the network, the buggy fold, and the fixed one:

use std::collections::BTreeMap;

const WORKERS: u64 = 3;
const REPORTS: u64 = 200; // cumulative reports per worker: 1, 2, ..., 200

// One report: (worker id, that worker's cumulative processed count).
type Report = (u64, u64);

fn produced_order() -> Vec<Report> {
    // Round-robin interleave: the order the workers actually sent.
    (1..=REPORTS)
        .flat_map(|n| (0..WORKERS).map(move |w| (w, n)))
        .collect()
}

// Deterministic Fisher-Yates driven by a tiny LCG: models a fan-in where
// per-message delays (retries, multiple hops) can reorder anything.
fn network_reorder(mut msgs: Vec<Report>, mut seed: u64) -> Vec<Report> {
    for i in (1..msgs.len()).rev() {
        seed = seed.wrapping_mul(6364136223846793005).wrapping_add(1442695040888963407);
        msgs.swap(i, (seed >> 33) as usize % (i + 1));
    }
    msgs
}

// Aggregator 1: "the report I received last is the newest" (assignment).
// Correct only if arrival order matches send order.
fn last_arrival_wins(msgs: &[Report]) -> u64 {
    let mut state = BTreeMap::new();
    for &(w, n) in msgs {
        state.insert(w, n); // <- the latent bug: overwrite trusts arrival order
    }
    state.values().sum()
}

// Aggregator 2: merge with max. Cumulative counters only grow, so the
// newest value is the largest one -- no matter when it arrives.
fn max_merge(msgs: &[Report]) -> u64 {
    let mut state = BTreeMap::new();
    for &(w, n) in msgs {
        let slot = state.entry(w).or_insert(0);
        *slot = n.max(*slot); // commutative + idempotent merge
    }
    state.values().sum()
}

fn main() {
    let expected = WORKERS * REPORTS; // 600
    let in_order = produced_order();
    let reordered = network_reorder(in_order.clone(), 42);

    println!("expected total:                 {expected}");
    println!("last-arrival-wins, in order:    {}", last_arrival_wins(&in_order));
    println!("last-arrival-wins, reordered:   {}", last_arrival_wins(&reordered));
    println!("max-merge, in order:            {}", max_merge(&in_order));
    println!("max-merge, reordered:           {}", max_merge(&reordered));

    // The tests this post is really about:
    assert_eq!(last_arrival_wins(&in_order), expected); // passes CI forever
    assert_ne!(last_arrival_wins(&reordered), expected); // the planted bug, reproduced
    assert_eq!(max_merge(&in_order), expected);
    assert_eq!(max_merge(&reordered), expected); // order-free merge stays right
    println!("assertions passed: the bug is arrival-order dependence, not math");
}

Run it with rustc reorder.rs && ./reorder.

On Rust 1.95.0 the output is: expected 600, last-arrival-wins answers 600 in order and 291 reordered, max-merge answers 600 both times. The wrong answer is not slightly wrong; it is a 51% undercount, because for each worker whatever report happened to arrive last — say the 97th of 200 — overwrote every later one.

Two details in that file carry the argument. First, the in-order assertion on the buggy fold passes. This bug ships. Any test that feeds messages through an in-process channel will approve it, which is why I call it a latent bug rather than a broken build. Second, when I widened the check to 1,000 different reorder seeds in my own testing, last_arrival_wins was wrong under all 1,000 of them and max_merge was right under all 1,000 — including a run where I delivered every message twice. The fix is not cleverness; it is choosing a merge function where arrival order and duplication stop mattering. That is the same lesson CRDTs teach, shrunk to one BTreeMap entry.

The problem is that nothing in Rust, or in any mainstream language, connects the state.insert(w, n) line to the delivery contract of the channel feeding it. The invariant lives in my head. The type checker sees a perfectly fine map write.

The port: where the type checker stopped me

Hydro is a Rust framework out of UC Berkeley's dataflow research lineage. You write one program describing computation across locations — a Process here, a Cluster of workers there — in choreographic style, and a staged compiler splits it into per-machine binaries. That architecture is not today's subject; the type of one value is.

In Hydro, the aggregator's inbox is not an iterator of messages. It is a Stream with five type parameters:

Stream<Type, Loc, Bound = Unbounded, Order = TotalOrder, Retry = ExactlyOnce>

Order and Retry are the two that killed my bug. A stream is marked TotalOrder only when no nondeterminism can affect element order; a merged fan-in is marked NoOrder. Duplication works the same way: ExactlyOnce versus AtLeastOnce. These markers are not documentation. Operators consume them, and the network operators degrade them to match what the wire can promise.

The port of my workers-to-aggregator hop looks like this:

let totals = workers
    .source_iter(q!(local_reports()))   // Stream<(u32, u64), Cluster<Worker>, ...>
    .send_bincode(&aggregator)          // KeyedStream<MemberId<Worker>, (u32, u64), ...>
    .values();                          // Stream<(u32, u64), _, Unbounded, NoOrder>

let state = totals.fold(
    q!(|| BTreeMap::<u32, u64>::new()),
    q!(|m, (w, v)| { m.insert(w, v); }), // the same buggy line, ported
);

Sending from a cluster to a process returns a KeyedStream keyed by sender: per-member substreams keep their order over the default fail-stop TCP transport, because one TCP connection does deliver in order. But the moment I call .values() to merge everything into one bus — which is exactly what my hand-rolled mpsc fan-in did implicitly — the result is typed NoOrder. The interleaving across senders is nondeterministic, and now the value's type admits it.

And on a NoOrder stream, that fold does not compile. The error, abridged from the repository's own compile-fail test suite, reads:

error[E0277]: Because the input stream has ordering `NoOrder`, the closure
              must demonstrate commutativity with a `commutative = ...` annotation.
   = note: To intentionally process the stream by observing a non-deterministic
           (shuffled) order of elements, use `.assume_ordering`. This introduces
           non-determinism so avoid unless necessary.

This is the moment the experiment was for. The compiler is not saying my closure is wrong. It is saying my closure's correctness depends on an ordering this stream does not have, and it refuses to proceed until that dependency is resolved. Map insertion with overwrite is not commutative — insert(w, 97) then insert(w, 200) differs from the reverse — so no truthful annotation lets the bug through intact.

The diagram below is the picture worth holding: per-sender lanes keep their order, the merge discards it, and the fold gate refuses to open without a commutativity annotation. From that dead end the type system leaves exactly three exits, and each one is a legible design decision where the original code had an invisible assumption.

​

The first exit is restructuring: skip .values(), stay on the KeyedStream, and fold per sender, where per-key order is still TotalOrder and assignment is legal. That is a real fix — it encodes "order holds within a sender, not across senders" in the program's shape. It also stops being available the moment the transport itself can reorder: swap the fail-stop TCP configuration for one of the lossy, arbitrarily-delayed transports in the repository's networking tests and the guarantee weakens in the types, because the delivery contract of the transport is part of the stream's type.

The second exit is the one my max_merge fix took: make the combinator commutative and say so.

let state = totals.fold(
    q!(|| BTreeMap::<u32, u64>::new()),
    q!(
        |m, (w, v)| {
            let slot = m.entry(w).or_insert(0);
            *slot = v.max(*slot);
        },
        commutative = manual_proof!(/** max-merge of monotone counters is commutative */)
    ),
);

The third exit is .assume_ordering, the explicit unsafe hatch, which the error message itself discourages. It exists, and it should: sometimes you know an ordering fact the types cannot see. But it takes a nondet! marker with a written justification, which means the assumption is greppable in review. My original bug was the silent version of exactly this annotation.

What the guarantee is — and what it only attests

Here is the taxonomy I came for. In the hand-rolled version, "assignment over an unordered merge" was representable, untested, and shipped. In the Hydro version it is unrepresentable by accident: you can only reach it by writing an annotation that names the risk. That distinction — impossible versus impossible-to-do-silently — is what correct-by-construction actually delivers here, and it is worth stating without marketing gloss.

Because the annotation is the load-bearing part, I went into the source to see what manual_proof! checks. Today: nothing. It takes a doc comment explaining why the property holds, and its registration hook is a no-op — the justification is for humans. A comment in fold's implementation says the ordering nondeterminism is instead exercised by the built-in simulator, and that a future version intends to make the proof mechanism dynamic. The repository's simulation tests back the first half: they run flows over lossy, arbitrarily-delayed transports and exhaustively explore delivery schedules, asserting that reorderings really occur and that consistency holds across them. So if I lie in a manual_proof!, the type checker will not catch me — the simulator is the layer designed to.

I find that honest and slightly deflating at once. The type system moves the ordering assumption out of my head and into a checked interface; the truth of my commutativity claim still rests on me, a test, or a future prover. The compiler error told me where to think. It did not do the thinking.

The seam costs are real too, and I would not wave them away. Everything inside q!(...) is staged code — Hydro's two-phase model runs your program once to plan the deployment, then generates per-machine binaries — and staged closures are where IDE support, stack traces, and borrow-checker errors get noticeably worse than plain Rust. The crate line is at 0.17.0-alpha; I read the API at a late-July 2026 commit, not from a stability promise. And the port is a rewrite, not a wrap: the framework owns your topology and main loop, so the adoption unit is a service, not a function.

One more boundary worth drawing, since I recently spent time model-checking a design in Quint: that tool checks a model of your protocol and leaves the implementation free to drift; Hydro types the implementation itself, but only for the properties its markers can express — ordering, duplication, boundedness. They attack different halves of the same gap. Neither will notice that your business logic computes the wrong number in a perfectly commutative way.

So does the port pay at small scale? For this service, on its own, a code-review rule — "merge, never assign, across a fan-in" — plus the 1,000-seed property test would have caught the same bug for a fraction of the learning curve. What the review rule cannot do is scale to code I did not review, which is Brooker's actual point about agents: when more of the code is written by something that does not attend design reviews, guarantees attached to the artifact beat guarantees attached to the culture. That argument gets stronger every quarter, and it is the reason this experiment goes in my notes as a genuine capability, alpha rough edges and all, rather than as research theater.

What I'm keeping

• The bug class to fear in fan-in code is arrival-order dependence: my planted version passed every in-order test and undercounted by 51% under a reorder. Reproduce reorderings deterministically; a seeded shuffle is enough.
• Cumulative reports plus a max merge make order and duplicates irrelevant. If your counters are monotone, you never needed "latest arrival" — you needed "largest value."
• Hydro's contribution is not magic verification. It is five type parameters on Stream that make delivery contracts part of the value's type, so unordered merges refuse non-commutative folds until you restructure, fix the merge, or sign an explicit assumption.
• manual_proof! is attestation, not proof — the honesty check today is the simulator that explores delivery schedules, not the type checker. Budget your trust accordingly.
• Reach for this when the ordering-sensitive surface is growing faster than your review capacity — many services, many hands, or agent-written code. Skip it when one reviewed service with a property test covers the same risk; the alpha-stage seam costs are the whole price, and on a small codebase they exceed the bug's expected cost.

Use it when correctness depends on delivery semantics across many fan-ins and many authors. Avoid it when you need API stability this year, your team is not ready to debug staged Rust, or a merge-function convention plus a reorder test already closes the gap.