Re: [isabelle] Isabelle Foundation & Certification

On Wed, 16 Sep 2015, Peter Lammich wrote:

As far as I know, there is a patch of KunÄar, which exists for more than
half a year now, which
 * ensures that consts/defs only produce conservative extensions
 * Does not slow down Isabelle significantly
 * Works with whole AFP and Isabelle-Library, i.e., is does not break
existing formalizations by being too restrictive.

However, it seems to be rejected or not given high priority by some main
Isabelle developers.

Can you quote precisely who said what? Otherwise we get into a situation of vague rumors and implicit accusations of unnamed people.

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".


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