Re: [isabelle] Isabelle Foundation & Certification



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.