Tutorial: A Hello World in Coq (with IO)
coq-blog.clarus.me