Full Disclosure mailing list archives
Re: proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too
From: Georgi Guninski <guninski () guninski com>
Date: Wed, 4 May 2011 12:49:16 +0300
On Tue, May 03, 2011 at 04:27:29PM +0300, Georgi Guninski wrote:
10x. what about this scenario, is it reallistic: i claim i have a proof of X. the proof is thousands of files. lambda.v is the plugin and coqc is invoked on only top.v ?
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. _______________________________________________ Full-Disclosure - We believe in it. Charter: http://lists.grok.org.uk/full-disclosure-charter.html Hosted and sponsored by Secunia - http://secunia.com/
Current thread:
- proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too Georgi Guninski (May 03)
- Re: proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too Andreas Bogk (May 03)
- Re: proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too Georgi Guninski (May 03)
- Re: proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too Georgi Guninski (May 04)
- Re: proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too Georgi Guninski (May 03)
- Re: proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too Andreas Bogk (May 03)