Re: [isabelle] Isabelle Foundation & Certification



On 16.09.2015 16:51, Makarius wrote:
> On Wed, 16 Sep 2015, Peter Lammich wrote:
>> If we would have integrated this patch earlier, we could have said:
>> There was an issue, but now it is fixed, and we even have a
>> (pen-and-paper) proof that it is sound now. So, anyone who reads the
>> paper would probably be happy, and the rumours spread would be somewhat
>> like: "The old Isabelle versions are unsound, you should update to
>> Isabelle-2015, this is provably sound now"
> 
> The last sentence is the opposite of what I am trying to point out on
> isabelle-users and on isabelle-dev for countless years. When there is an
> incident of some sort, and change might improve the situation or make it
> worse.  There is never a state where one could claim it to be "fixed".

We know that the current situation is bad -- at least, as long as one
wants to treat definitions as conservative extensions, which many of us
want to do. I understand there is a patch with a sound theory behind it,
which prohibits unsound definitions, without breaking current applications.

We may never achieve perfectness, there may be other issues, there may
be an even deeper change which would be even better. But I would expect
a critical (under the above assumptions) hole to be closed, as soon as
the problem is understood -- and not blocked on the vague notion that
every change may break something.

  -- Lars




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