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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and