Re: [isabelle] Where to learn about HOL vs FOL?



on 6/2/13 2:41 PM, Makarius <makarius at sketis.net> wrote:
> 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.

But Makarius, I merely mentioned Isabelle's priorities, to help explain some
background about its complexity.  You then questioned HOL Zero's
trustworthiness, then I responded.  So if you're getting tired of the
trustworthiness issue, then don't bring it up.

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

My point is that these changes, with their best of intentions, dominate the
implementation of Isabelle and yet make the implementation harder to
understand.  Therefore understandable implementation cannot be Isabelle's
*main* priority over the years.  The main priorities are things that are
driving these changes.

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

Pretty printing is very strongly related to trustworthiness!  If the pretty
printer prints one thing but internally it's something else, then the user
gets misled about what has been proved and/or what has beed defined.  I have
known examples on real industrial safety-critical projects where this has
caused problems.  It doesn't get much more serious than that.

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

Because these are all secondary issues, i.e. issue in the programs that fit
around the theorem prover rather in the theorem prover itself.  I'll say it
again, the primary trustworthiness issue in theorem prover implementation is
designing and implementing a system that itself has no intrinsic
trustworthiness-related flaws.  LCF-style architecture gets us a long way on
this count, but is not the end of the story because it does not address
pretty printer issues.

Mark.





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