I will give a very brief demo of the Coq interactive proof assistant. To illustrate how to work with Coq, I will formalize a simple compiler correctness proof from Graham Hutton's "Programming in Haskell". The Coq code is available here