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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and