This session illustrates the proof of simple imperative programs using Hoare logic both with the Coq proof assistant and the Why3 toolset.