Re: [isabelle] Isabelle Foundation & Certification



In the replied-to mail, I see more arguments that we should add proper
dependency checking to Isabelle/HOL as soon as possible.

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. 

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"

However, now we have: If you use overloading, you are basically on your
own, and have to ensure consistency yourself. Rules how to ensure
consistent definitions are not included in the Isabelle documentation.
And the rumours about Isabelle unsoundness spread as described in the
replied-to mail.

So if we want to use Isabelle as a device to get very high confidence in
our proofs, any mechanism that allows you to prove False in some
intransparent ways should be considered a severe malfunction of the
system, and fixed as soon as possible. And tainting an essential
mechanism as axiomatic (as the documentation of defs does) is not a
solution, but makes the system essentially unusable for getting
high-confidence theorems.

In my opinion, we should even think of a mode of operation that forbids
to add any axioms beyond a certain default set of axioms (e.g. HOL),
such that we can establish the guarantee: "Sound wrt. HOL", without
manually inspecting all theory files for axiomatic declarations (see
HOL-zero how to drive this idea to the extreme).

--
  Peter


On Mi, 2015-09-16 at 15:41 +0200, Burkhart Wolff wrote:
> Dear all, 
> 
> with respect to the debate around the paper by OndÅej KunÄar and Andrei Popescu: A Consistent Foundation for Isabelle/HOL (ITP 2015) 
> and the debate it created, I have the following remarks and informations to add:
> 
> 1) To be not misunderstood: I find this publication helpful and, after the quite nonchalant 
>     reactions of key members of the Isabelle Community, strictly speaking necessary.
> 
> 2) This paper creates outside the Isabelle community more echo than people might think.
>     At the moment, I am as part of the EUROMILS project part of the team that attempts
>     to get a common criteria (CC EAL5) evaluation for PikeOS through, where the models
>     and proofs were done with Isabelle. I can tell that I had a lengthy debate with
>     Evaluators and (indirectly) BSI representatives which became aware about this paper.
> 
>     And of course, there is the effect of a children's telephone game which distorts the 
>     story hopelessly.
> 
> 3) As part of the project, we wrote early a Recommandations-Whitepaper explaining the importance
>     of conservative extensions and trying to define something like a âsafe subsetâ of Isabelle. 
>     It is called:
> 
>         "Using Isabelle/HOL in Certification Processes: A System Description and Mandatory Recommendations" 
> 
>     and is part one of the EUROMILS Deliverable http://www.euromils.eu/downloads/Deliverables/Y2/2015-EM-UsedFormalMethods-WhitePaper.pdf <http://www.euromils.eu/downloads/Deliverables/Y2/2015-EM-UsedFormalMethods-WhitePaper.pdf>,
>    (pp. 1 .. 39)
>     a paper that is submitted to the ANSI and the BSI as part of the Common Criteria Evaluation of the PikeOS operating system.
>     It may be that these Mandatory recommendations were reused in future projects of this kind.
> 
>     In this paper, we ruled out the critical consts - defs combination as unsafe, and made sure that we did not use these constructs in
>     our entire theories (as well as axioms, etc. Restraining strictly to conservative extension and avoiding obfuscation).
> 
> 4) I welcome to see more formally proved meta-theory of Isabelleâs specification constructs; the HOL4 community shows at the
>     moment impressive progresses in this direction. May be that other open issues could be addressed as well. 
> 
> 
> Best regards,
> 
> Burkhart






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