The design of scientific experiments deserves its own variation of formal verification to catch cases where scientists made important mistakes, such as forgetting to take confounding variables into account. One of the most fundamental underpinnings of science is causality, or what it means for interventions in the world to cause other outcomes, as formalized by computer scientists like Judea Pearl. However, these ideas had not previously been made rigorous to the standards of the programming-languages community, where one expects a (syntactic) program analysis to be proved sound with respect to a natural semantics. In the domain of causality, as the relevant "program analysis," we focus on $d$-separation, a classic condition on graphs that can be used to decide when the design of an experiment controls for sufficiently many confounding variables, even though the reason that this condition works is often unintuitive. Our central result (mechanized in Rocq) is that $d$-separation exactly coincides with a novel semantic definition inspired by noninterference from the theory of security. This characterization provides a structural semantic foundation for $d$-separation and helps explain why the graph-theoretic condition is correct, independently of probabilistic assumptions. For each given automated test on the quality of an experiment design, our theorem justifies an associated method for falsifying the world-modeling hypothesis behind the experiment.

翻译：科学实验的设计需要其独有的形式验证变体，以捕捉科学家可能犯下的重大错误，例如忘记考虑混杂变量。科学最基本的基石之一是因果性，即世界上的干预如何导致其他结果，这一概念由朱迪亚·珀尔等计算机科学家形式化。然而，此前这些思想尚未达到编程语言社群所期望的严格标准，即（语法）程序分析应被证明相对于自然语义是可靠的。在因果性领域，我们关注作为相关“程序分析”的$d$-分离——一种关于图的经典条件，可用于判定实验设计是否控制了足够多的混杂变量，尽管该条件有效的缘由常不直观。我们的核心结果（已在Rocq中机械验证）表明，$d$-分离恰好与受安全理论中无干扰启发的全新语义定义完全一致。这一刻画为$d$-分离提供了结构性语义基础，并有助于解释该图论条件为何正确，而无需依赖概率假设。对于关于实验设计质量的每项自动化检验，我们的定理都证明了相应方法可用于证伪实验背后的世界建模假设。