Tacet: A Language and Type System for Automatic Statistical Validity Accounting
2026-08-27 • Programming Languages
Programming LanguagesSoftware Engineering
AI summaryⓘ
The authors present Tacet, a new language designed to improve the reliability of statistical claims in computer science research. Tacet requires analyses to explicitly state what data they use and what results they expect, rejecting claims that cannot be properly tested or justified. Their system uses a special math framework to track how data is used and to control errors in multiple comparisons, even letting researchers check their claims before running analyses. They proved their math correct with formal verification and illustrated the approach using real datasets. Overall, the authors aim to reduce hidden biases like cherry-picking by enforcing strict rules on how statistical evidence is presented.
statistical validitymultiple-comparison proceduresp-valuesformal verificationpre-registrationfunctional dependenciesstatistical testingtype systemsLean 4empirical evaluation
Authors
Chiké Abuah
Abstract
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.