Re: [isabelle] lexical matters
On 19/01/11 14:36, mark at proof-technologies.com wrote:
on 19/1/11 3:25 AM, Michael Norrish<Michael.Norrish at nicta.com.au> wrote:
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
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.
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.
Right, which is why we have the pretty-printing solution of my paragraph above.
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. My thought-experiment sexp-syntax would raise an exception if it encountered variable or constant names that were lexically bad. Overloads would not be printed at all. Instead, you'd get things like
(= (integer$+ (integer$int_of_num x) (integer$int_of_num y))
(integer$int_of_num (arithmetic$+ x y)))
This archive was generated by a fusion of
Pipermail (Mailman edition) and