Re: [isabelle] lexical matters



on 18/1/11 12:12 PM, Makarius <makarius at sketis.net> wrote:

> On Tue, 18 Jan 2011, mark at proof-technologies.com wrote:
>
>> Yes, I agree that the LCF style largely solves problems of
>> trustworthiness, and that the sort of problems it solves are the
>> most serious.  But given that this has been solved (a long time
>> ago), shouldn't we tackle the remaining problems?
>
> Trustworthiness is just one of many problems, and we have been
> able to increase it in Isabelle gradually over the years.
>
> Apart from that efficiency, accessibility, usability etc. are of general
> importance to make our arcane provers acceptable to more people
> out there.  I often find myself in the situation of a formalistic
> fundamentalist when speaking to people outside our community.

Yes, and I similarly.  There are people out there who simply don't want any
involvement with formal proof.  My fear is that, as we are trying to push
theorem proving more towards mainstream usage, sceptics will emerge citing
"well you can't even trust theorem provers anyway".  There was that debate
in the 1970s...

> E.g. when you start moving towards serious Prover IDEs, what I've been
> involved for quite some time now, you will find many more issues than the
> rather trivial parse/print problem of the low-level term language.

Yes, adding layers can present more problems, and I'm sure you have more
experience in this than me.  But surely we should be addressing these
problems as they arise, instead of brushing many of them under the carpet?
Shouldn't there be some sort of research effort concentrating on this?

> Of course, I always try to keep as much immediate reliability as possible.
> But I also feel one should separate concerns here: if you need extreme
> trustworthiness, then you should export full theory and proof content to
> some tiny external checker.  The latter does not even need concrete syntax
> in the traditional sense.

Unfortunately, the external checker needs to have a trustworthy printer
(despite that this has not traditionally been expressed as a priority).  It
needs to be able to print syntax in a highly readable way, so that a proof
auditor can effectively review exactly what the checker has checked.  A
large project involving formal proof might have hundreds of definitions that
need reviewing, as well as the end-result theorems that use these
definitions.  Wading through primitive syntax makes this an almost
impossible task.

> HOL0 could be one such checker, if it would be able to absorb huge
> theories and proofs (traces of inferences).  Then one could implement some
> "HOL0" button in Isabelle.

Well that's what I designed it for!  Being able to absorb huge theories is
of course crucial.  But also is being able to trust the inference kernel and
the pretty printer.  The HOL Zero button already exists in a prototype HOL
Light variant I developed.  Not so easy for Isabelle HOL....

Mark.





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