Abstract
Just as mathematical logic provides laws for reasoning about mathematical definitions and statements, a program logic for a programming language provides laws for establishing true properties of all possible executions of a program written in that language. After reviewing this deductive approach to program verification and the earliest of these logics, published by C.A.R. Hoare in 1969, this lecture showed how Hoare's logic applies to many control structures, including several forms of loops, with single-level or multi-level premature exit, but also to non-deterministic constructs such as Dijkstra's guarded commands, and right up to the asymmetric coroutines and cooperative threads seen in the second lecture. Even the " goto " branch can be specified in Hoare logic, with a few precautions.
The second part of the lecture introduced separation logic, a more recent program logic that makes it easier to reason about pointers (references) to mutable state and the proper use of computer system resources. We have studied how to reason in separation logic about imperative and functional programs using control operators such as " call/cc " or effect handlers, following the approaches published by Timany and Birkedal in 2019 and by de Vilhena and Pottier in 2021. As much as continuations that can be launched several times easily invalidate the usual rules of program logic, single-use continuations such as those used in OCaml 5 remain compatible with classic separation logic.
