May 2011 Archives
Tue May 31 12:58:59 EEST 2011
GET /bog HTTP/1.1" 404 281 "
GET /bog HTTP/1.1" 404 281 "
Виждал съм доста странни веб логове, но това ми дойде много:
GET /bog HTTP/1.1" 404 281 "
Точно пък на моя сайт :)
Ако авторът на заявката е загубил вярата си заради 404 Not Found може да опита пак.
Mon May 30 16:19:37 EEST 2011
Devolution
Devolution (biology)
lol [1]
argued that "Ladies and gentleman, devolution is not a theory but a cold fact … the ape devolved from man" [1]
this reminded me of the joke:
Q: what’s the difference between a swine and a man?
A: a swine can’t get as drunk as a man
на български:
-
Каква е разликата между мъжа и свинята?
-
Свинята не може да се напие като мъж.
Tue May 3 14:00:27 EEST 2011
proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too
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 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$ tail fib5.v Theorem really: True = False. Proof. intuition. Qed. 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
a.ml is at: http://j.ludost.net/blog/misc/a.ml tar with the proof is at: http://j.ludost.net/blog/misc/proof.tar