Re: [isabelle] Isabelle Foundation & Certification

I should mention that a lot of the issues and ideas mentioned in this thread
are discussed in my recent paper:


on 19/9/15 10:39 AM, Tjark Weber < at> wrote:

> On Wed, 2015-09-16 at 15:41 +0200, Burkhart Wolff wrote:
>>  "Using Isabelle/HOL in Certification Processes: A System Description
>>  and Mandatory Recommendations"
> Beyond the specific def/overloading issue, there is a more fundamental
> problem. Isabelle (and other proof assistants) have evolved in a social
> context where users typically act in good faith.
> It is a fact that is neither widely advertised nor, as far as I can
> tell, well-understood outside a small community that Isabelle theories
> are not actually machine-checked proofs. (Sure, theories may contain
> proofs that can be checked by Isabelle. But if someone gives you an
> Isabelle theory and claims that it proves, e.g, FLT, there is no
> machine that could decide this claim for you.)
> This can be addressed in various ways, of course. You give several
> pages of "methodological recommendations" in your white paper,
> essentially attempting to identify a safe subset of Isabelle/Isar. HOL
> Zero and proof terms are other approaches, with different drawbacks.
> Surely satisfactory solutions will be developed eventually, when people
> perceive this problem as sufficiently important.
> Best,
> Tjark

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