Re: [isabelle] Verify the legitimacy of a proof?



On 07/07/17 18:37, scott constable wrote:
> 
> possibly written by other persons with malicious intentions.

Isabelle does not protect against malicious intentions. It would require
a quite different system to do that, one that you won't like to use.

The other big provers (e.g. Coq) are similar in this respect.

HOL-Zero is a notable exception in targeting a market of potentially
malicious (ab-)users, but it is not a "big prover".


	Makarius




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