Re: [isabelle] lexical matters



Hi Mark,

This discussion is a bit strange. It seems this is mostly due to a conflation of at least three very different functionalities that you expect from a "theorem prover":

(a) Checking Proofs -- This requires a trusted inference kernel only, based on abstract syntax. No interesting parsing or pretty printing here. Challenges: Logical complexities, Performance, Keeping code simple and understandable.

(b) Developing Proofs -- This requires flexibility and automation, support for arbitrary user-level code, and a way to reduce everything to kernel-level inferences. Trusted pretty printing is not an issue here either. Instead I want as powerful tools as possible.

(c) Auditing Definitions and Theorem Statements -- This is mainly an interface problem of the auditor trying to understand what has been proved. Pretty printing plays a role here, but there are many other things. But note that proofs play no role here. This is just about definitions and theorem statements.

I hereby make the bold claim that any system trying to do any two of these things at the same time is bound to make some lousy compromises that aren't acceptable if you are really serious.

It happens that LCF-style provers traditionally try to do both (a) and (b), and they do make compromises. Bringing (c) into the picture and trying to add it into one of those systems would probably make the situation worse, not better. This is just an argument for a separate tool, which could be HOL0. I have the impression though that you are trying to address both (a) and (c) at the same time, which may lead to new lousy compromises.

The issues about someone maliciously attacking the kernel etc. are orthogonal and probably have standard solutions. Operating systems and security people can solve this as soon as it is important enough for someone to pay the price. But logicians are not the right people to do this.

If a trusted prettyprinter is deemed to be important tool for the auditor,
then the auditor can code one up, or look over your shoulder while
you code it.  It's a fairly simple task.

Mark Adams wrote:
Not so simple that existing theorem provers have trusted pretty printers
(other than HOL Zero)....

previously, Mark Adams wrote:
but just
a healthy degree of concern, especially when the problems can be easily
addressed.

So are you claiming that is it easily addressed or that it isn't??? Maybe your reasoning needs to be checked by a trusted kernel?

Anyway, what properties must a pretty printer have in order to be trustworthy? Is there anything formal to be said here apart from Freek Wiedijk's Pollack-consistency? Or is it just defined in terms of the attacks you happen to imagine right now? It would be interesting to read some details here instead of just a claim of how important it is.

Alex





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