Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning

Explore a groundbreaking 15-minute conference talk from OOPSLA1 2023 that introduces Outcome Logic (OL), a novel approach unifying correctness and incorrectness reasoning in program logics. Delve into how OL generalizes Hoare Logic, incorporating monadic and monoidal properties to capture computational effects and reason about outcomes and reachability. Discover how this unified theory expresses true positive bugs while maintaining correctness reasoning capabilities, and learn about its application to nondeterministic and probabilistic programs. Gain insights from the presenters' argument for OL as a new foundational theory in program verification, supported by proofs of its ability to disprove false specifications within its own framework.