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

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
    - Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert, Bruno Barras