2 Coq Basics
There are two themes that we’ll be alternating between:
learning the verification-integrated programming language we’ll use to build our verified compiler, and
learning the foundations of programming language theory in order to precisely define and state the compiler correctness property we hope to prove.
Eventually these two will intersect, but until then, we’ll be switching back and forth between the two themes.
Today we’re going to work on the first in hopes of getting you quickly up to speed.
We’re going to be using the Coq Proof Assistant as our verification-integrated programming language. Coq is one of the most mature and widely used langauges that fall within the verification-integrated family of languages and tools.
There are many advanced features, as well see in due time, but today I just want to give a sense of what it’s like using Coq to do some fairly mundane things that should feel pretty comfortable if you’ve used a statically typed functional programming language (e.g. OCaml) before.