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:

   www.proof-technologies.com/flyspeck/qed_paper.pdf

Mark.

on 19/9/15 10:39 AM, Tjark Weber <tjark.weber at it.uu.se> 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.