Re: [isabelle] Isabelle Foundation & Certification



Larry Paulson wrote:

> What we usually do to check a proof development is run âIsabelle buildâ and
> look at the output. Of course, Isabelle (and any system based on the LCF
> paradigm) allows arbitrary code execution. This should be borne in mind in
> connection with any idea that the use of a proof assistant eliminates the need to
> trust the person making the proof. None of us are developing software that has
> the remotest claim to satisfying any sort of security requirement.

Proof Carrying Code promised that the delivered code was accompanied by a proof that shows some security properties of the code. Its home page is outdated, does anybody know how far they went achieving this aim?

- Gergely


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