Skip to Content.
Sympa Menu

coq-club - Re: Re: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert

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.



Archive powered by MhonArc 2.6.16.

Top of Page