The Coq theorem prover is a powerful tool for verifying that program specifications satisfy various properties. In this presentation, I will introduce Coq using an example of verifying insertion sort. I will define a simple imperative language, a stack-machine language similar to Java bytecode, and a compilation process between them. The correctness of the compilation will then be proved. This demonstrates a very common technique in Coq, which has also been used to verify properties of LLVM bitcode and of operating systems.