Archive for April, 2012

Looking for students and postdocs

April 18, 2012

Work on exciting projects! Change the world!

Unfortunately, computing in Germany isn’t what it used to be in the 80’s. It can still be fun, though.

Advertisements

Rant

April 18, 2012

I saw the following (redacted, numbers modified) section in a recent paper doing a long proof in an interactive theorem prover:

Statistics

My proof, excluding standard libraries and the library for foobaring bazes, consists of 33 source files, 9 136 lines of specifications, 37 101 lines of proof, and 1 255 709 total characters. The size of the gzipped tarball (gzip -9) of all the source files is 135 009 bytes, which is an estimate of the information content of my proof.

 
 Call me a stat-hater, but I found the last line somewhat ridiculous. What next? Every paper must have a section
 
The size of the gzipped (gzip -9) pdf file for this paper is XXX bytes, which is an estimate of the information content of this paper.
 
A nice fixpoint problem to find XXX, though!