Re: [isabelle] Isabelle Foundation & Certification



On 17/09/15 15:35, Lars Noschinski wrote:
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


We tried it once on seL4. We ran out of memory (192GB, from memory) *very* quickly. It's currently impractical. A streaming approach might be better i.e. have the proof checker run simultaneously with Isabelle, and check every step taken by the kernel as it's made, without ever having to actually construct the whole proof term.

David




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