Re: [isabelle] Verify the legitimacy of a proof?



> However, we work with formal proofs, which can be examined, even
> interactively. We do not have to work on the basis that "X has been
> proved, therefore X is true", but rather "We have been given a proof
> of X; Is it credible?" Then we can look at any part of this proof
> where we have doubts. A devious user has many ways to try to fool us,
> but it's not so easy if he has to supply the full source code and we
> insist on legibility throughout. The effort we choose to invest in
> this would depend on how important X is and how much we distrust the
> person who supplied the proof.

Maybe it's time for an Underhanded Isabelle Contest?

<http://www.underhanded-c.org/>
<https://en.wikipedia.org/wiki/Underhanded_C_Contest>

Cheers
Lars




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