December 5th, 2008

beartato phd

(no subject)

A list of 100 theorems indicating which of them have been formally verified. Even though the list is of course rather arbitrary, I think this is a neat thing, inasmuch as benchmarks are better than nothing.

---

And if anyone finds themselves on cygwin and trying to follow the HOL Light tutorial, bear in mind you may need to follow the advice here and run ocamlmktop -o ocamlnum nums.cma from in /usr/bin.

Also where it says "if you are in Windows you should copy this file to pa_j.ml" that actively didn't work for me, and just running make seems to work so far.