Re: [isabelle] Isabelle Foundation & Certification
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.
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
> own definitions. I regularly see proofs that are valueless because they
> 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
> 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
> 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.
>> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and