lists.openwall.net | lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC | |
Open Source and information security mailing list archives
| ||
|
Message-ID: <20110504094916.GA5174@sivokote.iziade.m$> Date: Wed, 4 May 2011 12:49:16 +0300 From: Georgi Guninski <guninski@...inski.com> To: full-disclosure@...ts.grok.org.uk Subject: Re: proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too 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/
Powered by blists - more mailing lists