Re: [isabelle] Isabelle Foundation & Certification



Dear Burkhart,

I sympathise with you, but you go too far.

We do want tools such as Isabelle to be trusted by regulators and authorities. and so we do need to address every issue of this sort that comes along. Nevertheless, we should not be guaranteeing absolute certainty to anybody. If we oversell what is achievable, we risk a backlash.

It is true that it is now realistic to imagine fully verified proof checkers, the compilation to machine code also verified, running on a verified operating system and on verified hardware. Nevertheless, all of this involves using verification technology to verify itself. And there are innumerable other ways in which errors can creep in. Your âwithin a given modelâ is a huge qualification on "absolute certainty".

Avra Cohnâs 1989 essay on the subject remains topical:

http://www.cl.cam.ac.uk/~mjcg/papers/AvraProofPaper.pdf
http://link.springer.com/article/10.1007%2FBF00243000

There are any number of papers that report some of the gains that can be realised using verification tools, without making unrealistic promises.

Larry


> On 17 Sep 2015, at 13:35, Burkhart Wolff <Burkhart.Wolff at lri.fr> wrote:
> 
> I respectfully disagree.
> It poses an immediate problem for users who have to argue in front of
> certification authorities why using Isabelle may guarantee absolute certainty
> (within a given frame of an underlying logic and model). And this might be an
> important business case for the entire community.
> 
> Why Isabelle, if I could also apply BachblÃtentherapie to improve software quality ? 
> 
> If a definition makes SENSE (that is, in my view, indeed users responsibility) is just 
> another issue than that it makes an underlying theory inconsistent, which should
> be Isabelleâs responsibility if methodologically correctly used.
> 
> By the way, I support the proposal earlier made in this thread to have a
> âsafe_use_flagâ which restricts a session to constructs that we have reasons
> to believe that they are conservative.





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