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
this.

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 these".

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 trustworthiness.

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.


	Makarius






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.