Tutorial on implementing Hoare logic for imperative programs in Haskell

Using the programming language Haskell, we introduce an implementation for a simple imperative language that can evaluate arithmetic and boolean expressions; step by step, we will expand the implementation starting from arithmetic expressions, to boolean expressions and then to imperative programs. As we expand the language, we will show several evaluation strategies, considering the normalization property and how it affects an implementation. Finally, we will provide a bottom-up implementation of Hoare's logic which will allow us to deduce facts about programs without the need for a full evaluation.