[FOM] Formal verification

[Freek Wiedijk]

Dear Lasse,

>Is there a serious effort towards achieving a translation
>between the different systems, or at least building a
>system in which the current systems can both be interpreted?

There are projects like that, like the Logosphere project of
Carsten Schuermann (a modern variant of that being worked
on in the Dedukti project of Gilles Dowek), and things
like Joe Hurd's OpenTheory.  However, those projects are
not so much about the foundational issues, but more about
encoding the logics separately in one framework, but without
integrating them.

If you want to both have Coq and HOL proofs in one framework,
then it's like this:  Coq is much richer than HOL, so it's
easy to map HOL into Coq, and difficult to map Coq into HOL.
However, HOL is classical, and in Coq (even with HoTT)
there are many classically obvious things you cannot prove.
So interpreting HOL in vanilla Coq does not work either.

The obvious "system in which the current systems can
both be interpreted" would be Coq + sufficiently many
classical axioms added (maybe the Lean system that Jeremy
has been telling us about?)  However, the Coq type theory
is sufficiently foreign to HOL users that they won't be
very comfortable there.  And in the Coq community adding
axioms like that is very much frowned upon by the community.
For one thing, you lose the nice computational behavior.
So if you would do it like that, you would lose the Coq
users too.

Also, you would be working in a rather complicated
foundational world.  The typing rules for (co-)inductive
types of Coq are _not_ simple.  And the (sub-)typing rules
for the type universes of Coq are rather baroque as well :-)

Of course you could then embed such a "classical
Coq" in a version of ZFC with sufficiently many
inaccessibles (for the type universes), along the lines of
<http://www.cs.man.ac.uk/~petera/ts-st.ps.gz>.  That would
give Harvey his "golden standard" and also put you back in
a world with a reasonable logical foundation.  But that is
not being pursued by anyone, AFAIK.

Also there's currently no ZFC-based system that would
make the Coq and HOL users happy.  Maybe Isabelle/ZF comes
closest, but I think that has hardly any users.

Freek