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 може да опита пак.


Posted by joro | Permanent link

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

на български:

  • Каква е разликата между мъжа и свинята?

  • Свинята не може да се напие като мъж.


Posted by joro | Permanent link

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


Posted by joro | Permanent link