[FOM] proof assistants and foundations of mathematics

[Mario Carneiro]

On Wed, Aug 15, 2018 at 6:51 PM Timothy Y. Chow <tchow at math.princeton.edu>
wrote:

> > As far as (2) is concerned, it was pointed out by one of the
> > participants in this discussion that the responsibility for avoiding
> > such malignant routines is the programmer's, not CIC's.
>
> I'm not sure which "one of the participants in this discussion" you're
> referring to.


I think he is referring to Larry Paulson (specifically the "users should
take responsibility for their definitions" part). This also seems
reminiscent of the popular stance on the OCaml exploits of HOL/Light -
users should take care not to exploit any known bugs. I am neither a
HOL/Light nor Isabelle user though so take my reading of this position with
a grain of salt.

On Mon, Aug 6, 2018 at 5:40 PM Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> It's interesting to see a consistency claim stated in such an extreme
> form. Certainly these systems are designed with great care to be sound, and
> soundness bugs are taken very seriously. A couple of years ago, there was
> concern when it was discovered that a sufficiently devious Isabelle/HOL
> user could sneak in an elaborate form of circular definition, and from that
> prove 1=0. This is not my idea of a soundness bug (users should take
> responsibility for their definitions), but I agree that it deserved to be
> fixed. One has to be naïve to assume that no further bugs affecting
> soundness are present.
>

 Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180815/3829efe8/attachment.html>