This will be not so much a talk as a demonstration: in a nutshell, I'll show the Coq proof assistant. I will be talking about the theory and principles behind Coq, and will go through some examples to show how Coq works, what you can (and can't) do with it, and why it has won the ACM Software System Award in 2014.