Re: [isabelle] lexical matters



on 19/1/11 3:51 AM, Michael Norrish <Michael.Norrish at nicta.com.au> wrote:

> ...
>
>> Not sure what you mean here.  You seem to be saying that low-tech
>> printers are the way forward, which again seems to be suggesting
>> that good concrete syntax printers do not help human readability.
>
> Of course they do.  We also know that in our day-to-day use of our
systems,
> the pretty-printer is not a cause of problems, so we can use the nice
> readability-enhancing features of these systems.  On the other hand, if
> there is a worry about malicious attacks (as in the validated work
scenario)
> then people concerned about these things can print the terms in question
> using sexp-syntax, which we know to be adequate.

So if you recognise that good concrete-syntax pretty printers are generally
good for human readability, then this is also true for the proof auditor.
If we could have a trusted system that supports proof auditing AND has a
good trustworthy concrete-syntax printer, then isn't that the best of both
worlds?

>> All of the "3 HOLs" (presumably you are not including HOL Zero in the 3
>> HOLs :) have problems with printing irregular names, and all of them
>> have problems coping with overloaded variables.
>
> I guess you mean overloaded constants....

No, I mean variables that are overloaded with other variables.  The sort of
thing that basic Hindley-Milner type inference cannot deal with (but this is
for parsing so let's not get distracted by this).  Apart from HOL Zero, no
other system is capable of printing (or parsing, as it happens) an
expression with overloaded variables.

I suppose your low-tech s-exp printer would throw these out too.  It's
starting to be less trivial than originally envisaged.  Isn't it just best
to have a good trustworthy concrete-syntax printer?

Mark.





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