Technically, it is possible to prove anything in Coq proof assistant http ://coq.inria.fr due to a programming feature (or bug). This seems tractable when validating large proofs. Human analysis may catch this.
What are the consequences of technically proving anything in Coq?
More or less the question had in mind dishonest human provers presenting seemingly valid long computer readable proofs.
Later Coq developers replied `little hack'. I saw no official plans or replies of breaking the well formed proof (possibly because of backward compatibility being priority).
The basic technical details are: Hostile ocaml plugins (possibly disguised as proofs in
FILE.v) can generate their own
.vo proofs (of trivial statements), thus subverting
coqchk, and don't giving a chance of "
coqc" to even see the "anything proof". The plugin does this with
exit(2) after writing
.vo. This scenario seems interesting when validating large archives.
Here is a sample session, including links to full source code:
joro@j:/tmp/test1$ tar xvf ../proof.tar fib5.v bLOB joro@j:/tmp/test1$ ls -l total 16 -rwxr-xr-x 1 joro joro 10301 2011-05-03 12:53 bLOB -rw-r--r-- 1 joro joro 125 2011-05-03 12:53 fib5.v joro@j:/tmp/test1$ coqc fib5.v Trivially true. coqchk may pass joro@j:/tmp/test1$ ls -l total 24 -rwxr-xr-x 1 joro joro 10301 2011-05-03 12:53 bLOB -rw-r--r-- 1 joro joro 51 2011-05-03 12:55 fib5.glob -rw-r--r-- 1 joro joro 125 2011-05-03 12:53 fib5.v -rw------- 1 joro joro 812 2011-05-03 12:55 fib5.vo joro@j:/tmp/test1$ coqchk fib5 Welcome to Chicken 8.2pl1 (February 2010) [intern /tmp/test1/fib5.vo ... done] ...snip... Checking library: fib5 *** vo structure validated *** checking cst: <>.fib5.thm1 checking cst: <>.fib5.really Modules were successfully checked joro@j:/tmp/test1$cat fib5.v Theorem thm1: True. Proof. auto. Qed. Declare ML Module "bLOB" . Theorem really: True = False. Proof. intuition. Qed. #note: there is a zero byte at the end of "bLOB". in addition "bLOB" may be "aux.v" joro@j:/tmp/test1$ coqchk -v The Coq Proof Checker, version 8.2pl1 (February 2010) compiled on Feb 27 2010 16:09:50
to compile the plugin:
ocamlopt -o bLOB -shared a.ml
the plugin writes valid but unrelated .vo proof and then does
exit(2) to prevent
coqc from analyzing the "anything proof".
Possibly the most likely exploit scenario is:
Here is a proof of X consisting of about $10^5$ files.
lemma2817.v is the plugin and it doesn't stop the final proof.
Update Possibly a more portable solution (Coq):
Theorem really: True = False. Proof. external "/bin/sh" "ESCAPE_SEQ; write_vo_proof; nicely_kill_coq ;" True. (* this invokes /bin/sh *) Qed.