Re: [isabelle] Isabelle Foundation & Certification
I was talking here about
- (relative) consistency of the logic
- and it's safe extension schemes.
Short term goal: an agreement on the safe core (I e : kernel PLUS extension schemes) and on the methodological issues.
Formal proofs for that are challenging, but nowadays perfectly feasible.
I was NOT talking about implementation correctness of Isabelle "as is", I am perfectly aware
Of the quite monstrous proof task and the principle limits of such an approach (it's always going to be based on models ... Of the machine,
The compiler, etc.)
Still, On the long run, relative
Solutions along this line of research
will and should come even for implementation correctness of Isabelle.
Von meinem iPhone gesendet
> Am 17.09.2015 um 17:23 schrieb Larry Paulson <lp15 at cam.ac.uk>:
> 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:
> There are any number of papers that report some of the gains that can be realised using verification tools, without making unrealistic promises.
>> 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