Re: [isabelle] lexical matters
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
(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:
a healthy degree of concern, especially when the problems can be easily
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and