一句话：提出 Outcome Logic，统一正确性与不正确性推理，并证明错误规约可在其自身中证伪。
现有找 bug 的程序逻辑（如 Incorrectness Logic）通常将正确性与不正确性视为需要不同逻辑基础的对立概念。本文提出 Outcome Logic（OL），它是 Hoare Logic 的新泛化，同时具有 monadic 与 monoidal 结构：前者刻画计算效应，后者推理程序结果与可达性。OL 既能表达真阳性 bug，又保留正确性推理能力。作者证明，任何为假的 OL 规约都能在 OL 自身中被证伪，从而形式化其对正确性与不正确性推理的适用性。他们还用该框架推理非确定性与概率程序中的新型不正确性，并主张 OL 可作为统一正确性与不正确性推理的新基础理论。
Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring different logical foundations. In this paper, we argue that a single unified theory can be used for both correctness and incorrectness reasoning. We present Outcome Logic (OL), a novel generalization of Hoare Logic that is both monadic (to capture computational effects) and monoidal (to reason about outcomes and reachability). OL expresses true positive bugs, while retaining correctness reasoning abilities as well. To formalize the applicability of OL to both correctness and incorrectness, we prove that any false OL specification can be disproven in OL itself. We also use our framework to reason about new types of incorrectness in nondeterministic and probabilistic programs. Given these advances, we advocate for OL as a new foundational theory of correctness and incorrectness.
@article{paperbot2026,
title = {Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning},
author = {Noam Zilberstein and Derek Dreyer and Alexandra Silva},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA1},
year = {2023},
doi = {10.1145/3586045}
}