Re: [isabelle] Where to learn about HOL vs FOL?
On Tue, 5 Feb 2013, "Mark" wrote:
That was quite an aggressive email. I feel I have to respond to your
points in order to defend my work.
I don't know where you see the agression here. I am rather getting tired
about the topic, because it has made so little progress in the past 3
years, where it has occasionally shown up on the mailing lists.
You should also try to get Coq into the whole picture, because its user
base covers all of the HOLs and Isabelle taken together, and the system
and its logic is even more complex. So how about moving this thread to
coq-club as a change?
on 4/2/13 3:10 PM, Makarius <makarius at sketis.net> wrote:
This is just plain-old modularity taken seriously.
The main priority? I don't believe that! You've already said that you
don't understand everything. The extra layers that have been introduced
massively complicate the implementation, but are done with the good
intention of improving usability (and maybe other reasons as well).
It is important to discern complexity vs. complication. Isabelle was not
done the way like "this is a good day to introduce some new layers to
complicate things; we are so smart, and it was hard to write so it should
be hard to read".
On the contrary, the "layers" were always an answer to genuine
complication that had occumulated over time, to rationalize and
systematize concepts etc. Doing this sucessfully then turns complications
into mere complexity. And modularity taken seriously means you only need
to understand layers separately and the principles of composition, but not
the whole of the result.
So, if understandable implementation were the *main* priority then why
on Earth would this have been done?
To keep the system alive and thriving over a very long time, with ever
growing demands from the applications. Isabelle has an unbroken tradition
of more than 25 years, always with the same code-base. Internally it
looks rather young, fresh, and clean, if you compare it to other systems
of such an age. For example, I am now routinely exposed to Java and its
standard libraries, and that is really complicated, not just complex.
As far as I understand, the only trustworthiness issue that you have with
HOL Zero is that it is implemented in OCaml. Firstly, HOL Zero addresses
the main OCaml vulnerabilities to do with string and integer representation,
and in any case can be relatively easily ported to SML, and I even intend to
do this at some stage, as you well know, so please stop banging on about
The string and int problem is a good example for genuine complication: you
have to "repair" bad effects from OCaml, but you don't want that extra
stuff there. The Coq guys have quite a few such repairs of OCaml in their
code. To make HOL Zero on OCaml really bullet-proof you would probably
have to blow up the kernel by a factor of 2 compared to a pure version,
lets say in SML, or even HOL as specification language.
I have pointed out further nasty tricks of OCaml occasionally, where you
simply cannot trust your eyes reading the OCaml source. Some LRI guys are
particularly good at playing such tricks and proud of it.
The primary problem is designing and implementing a system that itself
has no intrinsic trustworthiness-related flaws. All other HOL systems
other than HOL Zero have not managed to do this because they have flaws
in their pretty printer/concrete syntax design. Their implementors
either admit these flaws or brush them under the carpet with "well
normal users are not malicious so would never in practice exploit
I am one of thos who brush it under the carpet, because it is no real
problem in practice, but there are others. Pinning down parsing / pretty
printing like that is neither necessary nor sufficient for
I did see real issues in a different area, e.g. when Oracle (via the JVM)
bombs your GUI display somehow, so that you see an outdated version of
prover output. But the HOL-Zero approach does not cover prover IDE
connectivity at all.
This archive was generated by a fusion of
Pipermail (Mailman edition) and