Re: [isabelle] lexical matters

On Tue, 18 Jan 2011, Tjark Weber wrote:

On Mon, 2011-01-17 at 22:34 +0000, mark at 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 misleading?

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 does not sound like you are speaking here about Isabelle at all. We do not assume a "non-malicious" user. You can always inspect internal certificates, even before embarking on full proof terms.


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