Rant

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!
Advertisements

One Response to “Rant”

  1. SG Says:

    Á propos, http://xkcd.com/688/

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s


%d bloggers like this: