Posted by Georgi Guninski on May 03
proving _anything_ in the Coq proof assistant (in addition to code execution). « coqchk'' passes too
if some poor soul needs help with a coq [1] homework, this may help.
if some poor AV vendor need a proof his solution is bullet proof this may help too…
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…
Source: proving _anything_ in the Coq proof assistant (in addition to code execution). « coqchk » passes too
