Re: [isabelle] lexical matters



On Tue, 2011-01-18 at 11:23 +0100, Makarius wrote:
> On Tue, 18 Jan 2011, Tjark Weber wrote:
> > As long as you assume a non-malicious user who wants to create a valid 
> > machine-checked proof, it is not much of an issue.
> 
> This does not sound like you are speaking here about Isabelle at all. We 
> do not assume a "non-malicious" user.  You can always inspect internal 
> certificates, even before embarking on full proof terms.

And a malicious user, by misusing ML in Isabelle theory files, couldn't
replace the functions that you would use to inspect internal
certificates -- or the entire inference kernel; or even the entire
Isabelle process -- with his own implementation?

Kind regards,
Tjark






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