Re: [isabelle] lexical matters
On 19/01/11 00:11, mark at proof-technologies.com wrote:
on 18/1/11 2:01 AM, Tjark Weber<webertj at in.tum.de> wrote:
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.
Yes, but I don't think we can assume a non-malicious user! What if someone
wants to claim they have proved something in order to get paid?
Subcontracting out proofs could be a serious business in the future.
If the contractor's product is being audited sufficiently carefully, the auditor will notice the dubious calls to the pretty-printing/bare-ML infrastructure that were required to get the fake result looking acceptable.
I really do not believe that this is an interesting issue.
If the terms are really so large that printing them in "raw" form is likely to be a problem, then they will be just as incomprehensible in pretty form, and just as unreliable when checked by eye-balling. In that situation, the client will presumably check their supplier's work by doing something like
if aconv myterm (concl suppliers_thm) then print "OK"
else print "FAILURE"
And voilà, the pretty-printing "issue" disappears.
This archive was generated by a fusion of
Pipermail (Mailman edition) and