Evidence belongs in the result

Three programming-languages papers from this summer agree on a house rule I want everywhere: a claim does not count as a result until it carries something a defined checker can inspect. Hold that rule up against a typical generated bug report — severity, file, line number, three confident paragraphs about why the crash is real — and the report has nothing to offer it. The prose ranks the candidate, and accepting the claim still costs you the entire search the producer already ran.

The interface is the part I want to steal. The system proposing the bug, the bound, or the test may stay probabilistic, untrusted, as hallucination-prone as it likes, because acceptance runs through a small checker whose failure is explicit. A missing witness is an incomplete result, and an incomplete result is the producer's problem — which is exactly where that problem belongs.

Reachability belongs beside the bug#

Mizzle aims at the false alarms of agentic bug finding. It defines an incorrectness separation logic for a substantial subset of concurrent OCaml, so a bug report has to carry a derivation showing that an incorrect execution — stuckness, a race, non-linearizable behavior — is actually reachable. No derivation, no bug.

The authors mechanize the logic in Rocq on Iris and prove it sound and complete for their model, so a derivation cannot justify a false alarm and every modeled incorrect execution admits one. As far as I can tell the LLM experiment is a proof of concept, and nobody is claiming that proof search scales across an arbitrary repository yet. What has already changed is the reviewer's position: acceptance ends at a proof checker instead of at persuasive prose.

Different claims, different witnesses#

Parcas makes the same demand of performance claims. Parallel cost has two currencies — total work adds across child tasks, while span follows the longest dependency chain — and a bound is only honest if it accounts for both.

work(left || right) = work(left) + work(right)span(left || right) = max(span(left), span(right))

Work credits split additively, the easy half. For span, Parcas duplicates credits at each fork, tags every copy with a logical task identifier, and restricts where those credits may be spent or transferred. What comes out is a machine-independent work-and-span bound with a proof attached, rather than one flattering wall-clock number from the authors' hardware.

The third paper, a complexity theory of randomised testing, points the question at generators: being able to decide whether a value satisfies a predicate does not mean you can efficiently produce such values. Under standard cryptographic assumptions there are languages in P with no efficient generator, and efficient generability is characterized by a certificate scheme over a verifier.

That result explains why witness planting works — construct the evidence first, then derive a valid test around it. It also quietly kills a property-testing API everyone keeps wishing for: no general library can compose efficient generators out of arbitrary predicate conjunctions and negations, under the paper's assumptions — the wished-for combinator turns out to be cryptographically hard.

None of this makes evidence cheap to produce. Proof search can dominate the bug finding, logical credits want specifications, and a certificate-based generator still needs a construction that reaches the interesting cases. The cost moves upstream, though, and the report in your queue either has the derivation field or it does not — you no longer have to argue with its adjectives.