Re: [isabelle] Isabelle Foundation & Certification



Let me add to this discussion, just because I happen to have been
discussing it at Data61 yesterday too.

Yesterday, I showed my colleagues that it is possible to prove False in
Isabelle2015 without any warnings or errors and without any use of
axiomatization or oracles. The trick was, of course, Ondrej's example, but
updated to use "overloading" rather than the deprecated "defs" keyword.
Many of them were surprised, and wanted to know why, when I said that a
patch did exist, it has not been incorporated. I think rumours about
"Isabelle developers" are unavoidable at that point. We are also interested
in the opinion of qualifiers and regulators of the tools we use, and
Burkhart's original message is very interesting from that perspective.

My own opinion now: I would like the patch intended to make it impossible
to prove False in Isabelle/HOL no matter what definitions one uses
incorporated as soon as possible. I'm surprised that that is a contentious
issue. I believe we have found the last of those problems now, because of
Ondrej and Andrei's (on paper) consistency proof.

In the longer term, I am very interested in mechanising the consistency
proof (as we have done for the basic HOL logic as used in HOL Light).
Furthermore, if there is enough community interest, I would be interested
in building a verified proof-checker for Isabelle/HOL. One crucial
ingredient required from the Isabelle community here is the ability to
export proofs in a low-level format (ideally OpenTheory, rather than some
other new format), but I believe you're already quite close to that with
the option to produce proof terms.

I think this story involving explicit proofs and small verified checkers is
the ultimate one to sell to certification authorities, even while
day-to-day we also want our big tools to be sound.



On 17 September 2015 at 03:30, "Mark Adams" <mark at proof-technologies.com>
wrote:

> I think there is an important distinction here between getting a definition
> wrong and making the logic inconsistent.  Of course a user can always
> accidentally make a wrong definition, and of course this is a big problem
> is
> usage of theorem provers, but this is a red herring.  Users rightly expect
> that it should not be possible for definitions to make the logic
> inconsistent.  This, surely, is one of the big selling points of using
> definitional facilities as opposed to just adding axioms - they are (or
> should be) fundamentally conservative.  And this is why it was so important
> to fix the bug in HOL's primitive constant definition facility in the late
> 1980s, where type variables occurring in the RHS were allowed not to occur
> in the LHS.
>
> Mark Adams.
>
> on 16/9/15 5:25 PM, Larry Paulson <lp15 at cam.ac.uk> wrote:
>
> > Iâd like to point out again that users need to take responsibility for
> their
> > own definitions. I regularly see proofs that are valueless because they
> are
> > based on incorrect definitions.
> >
> > To my mind, a soundness bug is when a valid expression or proof state is
> > transformed into something wrong. The problem identified here are that
> > Isabelle is failing to prohibit certain definitions that donât make
> sense.
> > There is no claim that Isabelle is doing anything wrong with these
> > definitions. Itâs hard to believe that a user could make such definitions
> > accidentally.
> >
> > It would be interesting to find out how these problems were identified:
> > whether they were looked for out of curiosity, or whether on the other
> hand
> > they manifested themselves in the course of an actual proof.
> >
> > Larry Paulson
> >
> >> On 16 Sep 2015, at 16:39, Peter Lammich <lammich at in.tum.de> wrote:
> >>
> >> On Mi, 2015-09-16 at 16:10 +0100, Larry Paulson wrote:
> >>> I was under the impression that this patch had been adopted. I donât
> > believe that I saw any arguments against it.
> >>> Larry
> >>
> >> If this should be true, we should make it as public as possible, to stop
> >> any rumours about Isabelle unsoundness. The best way would be to release
> >> Isabelle2015-1 immediately, even if it would only be (Isabelle2015 +
> >> patch), and not based on the current state of the repository.
> >>
> >> --
> >>  Peter
> >>
> >
> >
> >
> >
>
>



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