I've seen some programming languages claim to be purely functional, but Coq has taken it to another level. This hello world tutorial *installs a third party library* so you can do IO! https://coq-blog.clarus.me/tutorial-a-hello-world-in-coq.html