First, I’m not (yet) an expert in formalized mathematics. I know Isabelle/ZF better, but have only overall view of Isabelle/HOL. Nevertheless I want to tell my opinion on typed (such as HOL) vs. untyped (such as Isabelle/ZF) systems.
Slawomir Kolodynski converted me into his religion of doing formalized math with Isabelle/ZF and answering “yes” to the question “Should the next generation of proof assistants be based on ZFC set theory?”, but now I resign.
The conclusion I drew recently: Doing math in untyped formalized systems such as ZFC is wrong. We need a typed system.
I drew this conclusion after my attempt to write a new version of “Funcoids and Reloids” (a draft article in the field of General Topology) presented on my site. I had the following trouble: Informal mathematics has no concept of types (not counting informal notion “dependent on the context” which is too raw to be used in complex enough cases like this my article). Without types it requires as I’ll show below to quality operations with a symbol denoting the context in which the operation is done. For an example, I need to write $latex \cap^L$ instead of just $latex \cap$ to denote the meet operation on the lattice $latex L$. The very trouble is with overlapping lattices, where it’s impossible to deduce which lattice is meant in $latex a\cap b$ as $latex a$ and $latex b$ may belong do different lattices.
Thus I did it in a wrong way, knowing that it is a wrong way. The reason I indeed has done it wrong is that there are just no concept of types in informal mathematics as it is presented customary. There are no way to do it in a right way without first introducing a formal system with types, which I cannot do in this article, because it is not an article about logic.
In this regard formalized math has an advantage over informal math, as statements of theorems and definitions can be write more concise in formal math thanks to types.
[This version of my article deleted as it is useless because my idea expressed in this post is wrong, see a comment.]
An example notation from the above mentioned article:
$latex ( \mathcal{A}_0 \times^{\mathsf{FCD} \left( A ; B \right)} \mathcal{B}_0) \cap^{\mathsf{FCD} \left( A ; B \right)} ( \mathcal{A}_1 \times^{\mathsf{FCD} \left( A ; B \right)} \mathcal{B}_1) = \\ ( \mathcal{A}_0 \cap^{\mathfrak{F} \left( A \right)} \mathcal{A}_1) \times^{\mathsf{FCD} \left( A ; B \right)} ( \mathcal{B}_0 \cap^{\mathfrak{F} \left( B \right)} \mathcal{B}_1)$
(here $latex \mathfrak{F}(A)$ is roughly saying the set of filters on a set $latex A$ ordered reverse to set theoretic inclusion and $latex \mathsf{FCD}(A;B)$ means the set of funcoids from a set $latex A$ to a set $latex B$, for our consideration it does not matter what exactly are funcoids).
See long, dependent on arguments qualifiers on every operation? It is a thing we need to get rid of. See the above mentioned article for more examples with such long verbose formulas.
As I’ve said above Slawomir Kolodynski converted me into his religion of doing formalized math with Isabelle/ZF, but now I resign. My new ideology is that we should try to make formalized math in Isabelle/HOL (including HOLZF).
Speculating in an area I do not know as an expert, I think we should do sets (in the sense of ZF sets) in HOLZF, but wrap some of them into HOL types.
Before ZF was seeming feasible for me, because I introduced the concept of generalization in the framework of ZF. This my result was looking for me as a solution of all typing problems. Now I realize, it isn’t. The above mentioned General Topology article cannot be written concisely in ZF without types.
Indeed a problem which my theory of generalization solves well is whole numbers generalizing natural numbers, rational numbers generalizing whole numbers, real numbers generalizing rational numbers, complex numbers generalizing real numbers, etc.
I does not work well with the theory of lattices and filters (for the reason that for example as lattice meet operation may mean different for the same arguments of the operation, because its meaning is different for different (overlapping) lattices).
Maybe we need to invent some new system having advantage of both untyped and typed systems. As a temporary solution I suggest as I wrote above to wrap HOLZF set values inside strong types. Is this working well? I don’t know.
Finally, I call you to discuss this topic in blogs and mailing lists.
My post was discussed in a mailing list:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-July/msg00036.html
My dilettante opinion was shown to be wrong.
I think you shouldn’t go from one extreme to the other so fast. Indeed discussing which foundation is best is a bit like discussing religions. The best approach is to try this, try that, and then choose what is best suited for your mind set and problem domain.
As for the “long, dependent on arguments qualifiers on every operation” I think this is more of a presentation problem than the foundation problem. Humans are very good at figuring out certain details from context. If those details don’t contribute to understanding of the proof they should be suppressed by the presentation layer. That fixes the problem on the reader side. On the writer side it is more difficult to fix and it may be unavoidable to tell the proof assistant exactly what you mean.
Many people think it is a good idea to layer some type system on top of untyped set theory, see Sebastian Reichelt’s HLM and ZPC by Jeremy Bem.
My idea was completely wrong. The source of my trouble was that I had overlapping sets. The solution is to use bijective copies of the sets to make them disjoint and this works in ZF (no need for a typed system for this).