This is the code repository for a toy compiler verification. It has a compiler
for arithmetic expressions to a tiny stack machine (idea came from Adam
Chlipala's CPDT) implemented in Haskell (in
src/Compiler.hs) that is then converted to Coq (using the
hs-to-coq tool by Spector-Zabusky,
Breitner, Rizkallah, and Weirich, with result
src/Compiler.v) and verified in Coq (proofs in
The proofs follow a style that is essentially a modified version of the proof style advocated by Adam Chlipala in Certified Programming with Dependent Types -- modified slightly in that hints are always kept extremely locally scoped. The intention behind this (explained a little further in the library repository for the couple tactics that implement this: dbp/literatecoq) is to make reading proofs be as easy as possible, where on paper you would write "follows by induction using X, Y, and Z". When hints end up in global databases, you can end up writing proofs that say "follows by induction using X, Z", because you had hinted Y somewhere earlier.
The accompanying writeup for this compiler is at https://dbp.io/essays/2018-01-16-how-to-prove-a-compiler-correct.html.
Download the submodules that contain the versions of
hs-to-coq and the
literatecoq tactics with:
git submodule init git submodule update
Then you need to both build
stack setup --resolver lts-8.3 STACK_YAML=hs-to-coq/stack.yaml stack build
And get Coq 8.6 and accompanying libraries:
opam repo add coq-released https://coq.inria.fr/opam/released opam update && opam install coq.8.6 coq-mathcomp-ssreflect.1.6.1
Once Coq has been installed, you can compile the base library for
(which essentially means that your converted programs can use elements of
make -C hs-to-coq/base
Finally, build the
make -C literatecoq
To convert the Haskell source to Coq, run:
STACK_YAML=hs-to-coq/stack.yaml stack exec hs-to-coq -- -o src/ src/Compiler.hs -e hs-to-coq/base/edits
This will put
To compile this (so you can work on proofs), run:
After which you can open up
src/Proofs.v in your chosen interactive frontend.
make will probably end with an error if you have changed things, as
it tries to run
Proofs through Coq as well, and if there are theorems that no
longer hold that won't work. But it will have built
src/Compiler.vo which is
what you need.
Obviously, this tiny example is not going to teach you how to prove things in Coq! There are various resources how to do that. A good one that used to not be online but now seems to be is Bertot and Casteron's Coq'Art: Interactive Theorem Proving and Program Development. Classics that have always been online are Certified Programming with Dependent Types and Software Foundations. Theorem proving (of which I'm still quite new at) seems to be a skill that relies on three pretty different skills: deep understanding of typed functional programming concepts, normal paper-and-pencil proof strategy, and understanding the abilities / quirks of the particular system you are using.