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
in `src/Compiler.v`

) and verified in Coq (proofs in `src/Proofs.v`

).

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.

This requires stack to install haskell
dependencies needed by `hs-to-coq`

(and maybe to experiment with the toy
compiler itself), and opam.

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 `hs-to-coq`

:

```
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 `hs-to-coq`

(which essentially means that your converted programs can use elements of
Haskell's `base`

library):

```
make -C hs-to-coq/base
```

Finally, build the `literatecoq`

library:

```
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 `Compiler.v`

into `src`

.

To compile this (so you can work on proofs), run:

```
make
```

After which you can open up `src/Proofs.v`

in your chosen interactive frontend.
Note that `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.

Related Awesome Lists

Top Programming Languages

Get A Weekly Email With Trending Projects For These Topics

No Spam. Unsubscribe easily at any time.

Haskell (20,939)

Coq (1,309)

Writeup (942)

Dependent Types (236)

Theorem Proving (111)