Re: [isabelle] Isabelle Foundation & Certification

Dear Larry,

> Of course I think that this circularity check ought to be made. I was under the impression that this patch had been made already. Nevertheless, I do not believe that it poses any immediate problem for users.

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.