Many interactive program verification tools are Hoare logic based. Hoare logics and their assertion languages can be formalized by either shallow embedding or deep embedding. The pros and cons of shallowly/deeply embedded formalization for assertion languages have been discussed for long time. But when it comes to the formalization for proof theories, tools like early versions of Verified Software Toolchain (VST), Iris-rust, Charge! etc. all choose shallow embedding to formalize their Hoare logics.

Some useful Hoare logic proof rules are nonderivable from primary rules. At the same time, their soundness proofs can be long and tedious. This talk introduces deeply embedded Hoare logics which solves this problem, avoid long, complex semantic reasoning and proves those rules as meta-properties. We have used this technique in the latest version of VST.