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.

Just another WordPress.com weblog

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

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!