Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning

Program logics for bug-similar to nding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring di similar to erent logical foundations. In this paper, we argue that a single uni similar to ed 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 e similar to ects) 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 speci similar to cation 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.