← All papers
First page of Tacet: A Language and Type System for Automatic Statistical Validity Accounting

Tacet: A Language and Type System for Automatic Statistical Validity Accounting

Chiké Abuah

cs.PL Aug 27, 2026 · v1 cs.SE
Metatheory of the Tacet type system and core calculus, including wealth-transformer properties, is machine-checked in Lean 4 with no admitted gaps.
Empirical comparisons between systems are a standard form of evidence in computer science research, but few are checked for statistical validity: most are never framed as statistical tests at all. Existing multiple-comparison procedures could control the resulting error, but need inputs (what an analysis examined, and how its observations are arranged) that are not recoverable from a list of p-values. We introduce Tacet, a language in which an analysis declares what it generated, states what it expects to find, and is refused any claim it cannot afford or cannot properly test. Its core calculus T pairs a free estimation sublanguage, carrying a reported footprint and a purity bit that records whether any outcome was consulted in building a value, with a priced claim sublanguage, carrying a wealth transformer, connected only by a mechanism that prices a comparison. A sample selected by reading outcomes sets the purity bit and is recorded as having examined everything it read, permanently, so it can never be granted a one-sided or confirmatory price, without the system ever asking whether the analyst intended to cherry-pick. Whether a comparison is paired or clustered is computed statically from the artifact schema, from declared functional dependencies between key fields alone and before any data is read, and a mechanism that assumes that structure away is refused rather than priced. Because the wealth transformer is antitone in the realized p-value, affordability can be checked before the analysis runs too, turning pre-registration into a typing rule. We prove the metatheory machine-checked in Lean 4 with no admitted gaps, and demonstrate the approach on a reference implementation and two case studies on published artifacts, the SWE-bench Verified leaderboard and BIG-Bench Hard.

Empirical system comparisons in CS are rarely checked for statistical validity, and standard multiple-comparison procedures require inputs (what an analysis examined, how observations are arranged) that cannot be recovered from a list of p-values alone.

Tacet is a language whose core calculus T pairs a free estimation sublanguage (tracking a footprint and a purity bit recording whether outcomes were consulted) with a priced claim sublanguage carrying a wealth transformer, linked only by a comparison-pricing mechanism. Paired versus clustered structure is computed statically from the artifact schema and declared functional dependencies before data is read. Because the wealth transformer is antitone in the realized p-value, affordability can be checked before running, turning pre-registration into a typing rule. The metatheory is proved machine-checked in Lean 4.

Three theorems are established, with the static under-approximation theorem and the wealth-transformer laws (monotone in W, antitone in p, no-refund lower bound) machine-checked in Lean 4 with no admitted gaps. A 1,994-line reference implementation is demonstrated on the SWE-bench Verified leaderboard and BIG-Bench Hard case studies.

orderingleaderboardBIG-Bench Hard
best first (oracle, invalid)6,545 of 8,91119 of 26
chronological/alphabetical0 of 8,91119 of 26
random, median [min–max]28 [0–302]17 [14–19]
as a reader meets them0 of 8,91119 of 26
worst first (oracle, invalid)0 of 8,91114 of 26
Affordable comparisons under different orderings