Re: [isabelle] lexical matters
On Mon, 2011-01-17 at 22:34 +0000, mark at proof-technologies.com wrote:
> It puzzles me how little has been done about these things until now.
> Are not people concerned that what is being displayed could be
Well, I for one think it's an unsatisfying design flaw in (some)
existing provers that one cannot trust their output.
In practice, however, this becomes a potential problem only when you
want to check a proof from an untrustworthy source. (Proof objects
provide a partial solution here.)
As long as you assume a non-malicious user who wants to create a valid
machine-checked proof, it is not much of an issue.
This archive was generated by a fusion of
Pipermail (Mailman edition) and