[FOM] Alternative Foundations/philosophical

[Freek Wiedijk]

Hi Tim,

>but my general impression is that the assistants that are
>based on type theory (not homotopy type theory) are easier
>to work with than Mizar, the best-known set-theoretical
>assistant.

Let me voice my not-so-unbiased opinions about this.

There are _two_ big groups of proof assistants, with other
systems next to those groups.  These two groups are:

- the type theoretical systems -- Coq, Agda, maybe NuPRL
  also still is being used (please tell me), and some
  experimental systems like Epigram and Cubical

- the HOL based systems -- Isabelle, HOL4, HOL Light,
  ProofPower (although I don't know how many users ProofPower
  still has), maybe PVS also could be considered in this
  group

So it's not "the type theoretical systems against the rest",
but "the type theoretical systems _and_ the HOL-based
systems against the rest".

Neither of these two groups are set theoretical, although
Coq has a consistency strength similar to set theory with
countably many universes.  Spiritually I consider the HOL
based systems "more set theoretical", although they have a
weaker expressivity (they only get you up to V_{omega+omega};
that might not matter too much when doing actual mathematics,
though).

Coq and Isabelle are _the_ two big proof assistants of today,
and seem similarly successful.  I wouldn't say that Coq is
more successful than Isabelle or the other way around.

Among the other systems, the set theoretical ones are:

- set theoretical systems -- Mizar, Isabelle/ZF,
  Isabelle/HOLZF (that's a fun foundations!), Metamath,
  maybe the B system also is in this group (although its
  foundations are somewhat weaker than ZF, close to HOL I
  think, spiritually it's very ZF-like)

These Isabelle systems are set theoretical incarnations
of Isabelle.  I don't think they have many users, but you
get some Isabelle-goodies when working with them, I think.
Maybe Makarius (if he's reading this) can tell us something
about that?

About Coq or Mizar being "easier": my opinion is that
(once you get past the hurdle of having Mizar parse your
statements at all), in Mizar it is much easier to "code"
a mathematical proof.  It's very close to just transcribing
the proof in Mizar syntax, and then "coloring it in", adding
intermediate steps and references between steps.  Also, Mizar
is much closer to how a mathematician experiences a proof.
Mizar is a mathematician's system, while Coq very much is
a computer scientist's system.

However, Coq has much stronger automation.  In Mizar you need
to do much more manually.  So in that sense Coq is "easier".
Someone who can deal with the weirdnesses of Coq, and doesn't
mind them, can get a formalization done much faster there.

I think that this difference in automation is orthogonal to
the foundations, though.  A set theoretical system with the
level of automation of Coq or Isabelle is very well possible.
It just hasn't been made.

I would say that for computer science proofs (like formal
semantics, or metatheory of logical systems) Coq is _much_
easier than Mizar.  However, for abstract mathematics (say,
topology; the system was created by a topologist), Mizar
would be... well, not _easier_ but much more friendly.
At the very least you get much more control over your proofs.

But note that Isabelle is very close to Mizar in its proof
language, _and_ Isabelle _does_ rival the automation of Coq.
So maybe Isabelle is the easiest of all.  At least it is
very classical, foundationally, and not "weird" at all.

Freek