Re: [isabelle] Isabelle Foundation & Certification



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.