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.

Michael





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