Re: [isabelle] lexical matters



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

> On 19/01/11 14:04, mark at proof-technologies.com wrote:
>
>>I never thought that advocating a trustworthy pretty printer would be so
>> controversial!!!
>
> It's just not an interesting problem.  We can solve it trivially by
writing
> everything out in sexp-like notation.  ACL2 is demonstrably an acceptable
> format for security-critical validation, and this is all the
pretty-printing
> they have.

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.

> Moreover, with proof terms (in Isabelle) and things like OpenTheory for
the
> 3 HOLs, we can avoid having to look at clients' ML code.

I am also advocating proof porting.  With proof porting, however, we have
the same problem - in the target system, we still need to know that the
ported theorem is the right one and that the ported definitions are right.

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.

Mark.





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