I will describe work in progress on Osiris, an attempt to equip a nontrivial fragment of OCaml with a formal semantics and with an interactive program verification environment, hosted inside the Rocq proof assistant. Our semantics is hybrid: it takes the form of a monadic interpreter, defined on top of an ad hoc monad, whose semantics is given by a small-step reduction relation. On top of this semantics, we define two program logics: a total Hoare logic, restricted to pure expressions; and a separation logic, based on Iris, for arbitrary expressions.
This is joint work with Jean-Marie Madiot, François Pottier, and Irene Yoon.
