Re: [isabelle] lexical matters



on 19/1/11 5:22 AM, Konrad Slind <konrad.slind at gmail.com> wrote:

> 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.

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

I think it would be an excellent use of formal methods to formally verify a
trusted pretty printer (such as HOL Zero's).  And, no, I'm wouldn't get
paranoid about how we trust the theorem prover used to do this.

Mark.





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