I will give an overview of an ongoing project to develop practical logics for reasoning about programs in large fragments of Standard ML. Our logics are inspired by ideas from denotational semantics, but they also admit a direct “operational” interpretation in terms of concepts familiar to programmers. As well as working out the details of these logics, we are currently developing machine support for them using the Isabelle generic theorem prover.
In this talk I will emphasize the way in which ideas from semantics can help us to design a proof system intended for non semantically inclined users.