Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
Thomas Powell
TL;DR
The paper addresses the challenge of extracting imperative programs from proofs by introducing SL, a first-order logic extension with abstract Hoare triples for state reasoning, and presents a stateful realizability interpretation into a mixed functional/imperative language ST via the state monad. It defines a soundness theorem linking provability in SL to stateful realizers in ST, and demonstrates an arithmetic extension featuring recursion and controlled while loops. The approach emphasizes abstraction and generality, offering a new perspective that complements verification-focused methods and outlines future directions such as probabilistic logic and computational semantics of proofs.
Abstract
We introduce an extension of first-order logic that comes equipped with additional predicates for reasoning about an abstract state. Sequents in the logic comprise a main formula together with pre- and postconditions in the style of Hoare logic, and the axioms and rules of the logic ensure that the assertions about the state compose in the correct way. The main result of the paper is a realizability interpretation of our logic that extracts programs into a mixed functional/imperative language. All programs expressible in this language act on the state in a sequential manner, and we make this intuition precise by interpreting them in a semantic metatheory using the state monad. Our basic framework is very general, and our intention is that it can be instantiated and extended in a variety of different ways. We outline in detail one such extension: A monadic version of Heyting arithmetic with a wellfounded while rule, and conclude by outlining several other directions for future work.