Re: [isabelle] Isabelle Foundation & Certification



On 17.09.2015 12:59, Ramana Kumar wrote:
> 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?

I am not aware of anyone doing that. As far as I can tell, we only ever
build Main with proof terms, and even that breaks frequently (by hitting
some resource limit).

  -- Lars




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