Re: [isabelle] lexical matters
On Tue, 18 Jan 2011, Tjark Weber wrote:
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 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