Re: [isabelle] Isabelle Foundation & Certification



Thanks Tjark.

I am aware of Stefan's excellent work, and I'm sorry if I gave the
impression that my proposal was novel in any sense. (Perhaps the part about
verifying the checker is new, but that's just icing for the purposes of
this discussion.)

My concern is whether the proof checker for proof terms is actually used or
not. In an ideal world, I would think that for any substantial
formalisation, the proof terms would be the bulk of the evidence provided
to the certification authority or any other party interested to know why
the claims being made are true, and those proof terms would be checked
regularly (say twice a year) by a small checker if the formalisation is
under continued development. Does anyone actually do that? Is scalability
the only issue?

Apologies if this is veering too far from the original topic. I'm happy to
continue discussion on another thread if desired.

On 17 September 2015 at 20:40, Tjark Weber <tjark.weber at it.uu.se> wrote:

> Ramana,
>
> On Thu, 2015-09-17 at 08:38 +1000, Ramana Kumar wrote:
> > Furthermore, if there is enough community interest, I would be interested
> > in building a verified proof-checker for Isabelle/HOL. One crucial
> > ingredient required from the Isabelle community here is the ability to
> > export proofs in a low-level format (ideally OpenTheory, rather than some
> > other new format), but I believe you're already quite close to that with
> > the option to produce proof terms.
>
> Take a look at Stefan Berghofer's thesis. He already implemented a
> proof checker for his proof terms (albeit not verified).
>
> The main issue, if I recall correctly, was that these proof terms could
> become huge.
>
> Best,
> Tjark
>
>
>



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