coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: Re: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert
chronological Thread
- From: guninski AT guninski.com
- To: coq-club AT inria.fr
- Subject: Re: Re: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert
- Date: Wed, 4 May 2011 13:50:13 +0200
if i read the fine manual, i would have saved myself the ocaml troubles
Theorem really: True = False.
Proof.
external "/bin/sh" "ESCAPE_SEQ; write_vo_proof; nicely_kill_coq ;" True.
(* this invokes /bin/sh. suited for formal software verification *)
Qed.
- Re: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert, guninski
- <Possible follow-ups>
- Re: Re: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert, guninski
- Re: Re: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert, Andreas Bogk
- Message not available
Archive powered by MhonArc 2.6.16.