[FOM] Formal verification

[Bas Spitters]

In addition to Freek's answer. Adding classical axioms to homotopy
type theory is discussed in the book (Ch10) and we do obtain a model
of either Lawvere structural set theory or CZF (+Grothendieck
universes) depending on how we set it up.

I am not sure how whether the (co-)inductive types of Coq and
(sub-)typing should be emphasized too much in comparison with CZF. In
this setting perhaps it suffices to mention W-types (M-types).
Coercive subtyping could be compared to CZF+Grothendieck universes.
If we want to dig deeper, I guess we should be comparing the
implementation of CZF in, say, Mizar with the implemention of type
theory in Coq.


On Wed, Oct 22, 2014 at 11:01 AM, Freek Wiedijk <freek at cs.ru.nl> wrote:
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom