Re: [isabelle] Isabelle Foundation & Certification



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

Unfortunately, there seems to be a lot of rumours, and these issues have
never been discussed openly. Also my knowledge is partially based on
rumours. Clear facts are the following:

In their paper [2], Popescu and Kuncar refer to a patch
http://www21.in.tum.de/~kuncar/documents/patch.html
and say: "it is currently evaluated at the Isabelle headquarters"

Since the paper was written about 6 month ago, and nothing has yet
happened in this direction [in my opinion, the patch should be
integrated as soon as possible, and Isabelle2015-1 released immediately!
], I concluded what I said above.



> 
> 
> > 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 generic and vague statement can be used as an argument against any
change, and against any argumentation why the change is necessary.

Let me try anyway: Most users of Isabelle expect that they cannot prove
False, unless they use some well-known unsafe methods, such as
axiomatization and oracles. This is a primary design goal of Isabelle.
This is supported, for example in [1], by the following statements:
  "The logical core is implemented according to the well-known âLCF
approachâ"

  "object-logics are specified by
stating their characteristic rules as new axioms. Any later additions in
application the-
ories are usually restricted to definitional specifications, and the
desired properties are
being proven explicitly"

The fact that one actually can prove false by using "defs", which is
commonly believed to be "definitional specification", is in strong
contrast to this goal. So, any state in which 
  1) all of Isabelle and AFP still works
  2) there are less possibilities to prove False in unexpected ways
is arguably an improvement, as it conforms more to a primary design
goal. Even if this improvement makes some aspects worse, one has to
weigh up those disadvantages with the advantage of making the system
more conforming to one of its primary design goals.


References:
[1] Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow:
  The Isabelle Framework. TPHOLs 2008: 33-38

[2] Ondrej Kuncar, Andrei Popescu:
A Consistent Foundation for Isabelle/HOL. ITP 2015: 234-252

--
  Peter





> 
> 
>  	Makarius






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