Re: [isabelle] lexical matters

> So if you recognise that good concrete-syntax pretty printers are generally
> good for human readability, then this is also true for the proof auditor.
> If we could have a trusted system that supports proof auditing AND has a
> good trustworthy concrete-syntax printer, then isn't that the best of both
> worlds?
If a trusted prettyprinter is deemed to be important tool for the auditor,
the auditor can code one up, or look over your shoulder while you code it.
It's a fairly simple task. Of course, for the paranoid, this just means
something else will emerge to be anxious about.


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