Re: [isabelle] lexical matters



on 18/1/11 10:52 PM, Michael Norrish <Michael.Norrish at nicta.com.au> wrote:

> On 19/01/11 00:11, mark at proof-technologies.com wrote:
> ...
>> 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.

The input to the process is raw ML code, and huge amounts of it.  Almost
anything can be hidden in this, unless very strict coding standards are
enforced.  It is a far nicer situation for the auditor to be able to treat
the ML code more-or-less as a black box, and review the state of the theorem
prover after it has supposedly established the end-result theorem.  I am
advocating a tool that makes life for the auditor easier.  A tool with a
pretty printer that can be trusted.

> 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,

You appear to be claiming that concrete syntax printers are of no practical
use to the human reader.

> 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.

Let's assume we don't trust the parser.  How do we know that 'myterm' is
correct?  We need to review definitions and terms, and this is best done
using a trustworthy pretty printer.

I never thought that advocating a trustworthy pretty printer would be so
controversial!!!

Mark.





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