How to make software without money

[Andrej Bauer <andrej...@andrej.com>]

Apologies for a slightly off topic post, but I think it is relevant to
many people on this list.

I just looked at some slides by William Stein, the author of Sage (an
open-source alternative to Mathematica) at
http://www.smbc-comics.com/index.php?id=4127

The conclusion is: it's impossible to make good quality software in
academia because there isn't enough money and because making software
doesn't give one any academic credit.

I am afraid formalization of math might fall into the same category,
unless we somehow elevate it to a "true science" level. A great deal
has been done in this respect recently by projects lead by Gonthier,
Hales and Voevodsky, but is it enough? Are we even making a dent?

At my department, for instance, the folk knowledge propagated from one
generation to another is that "someone" formalized "Landau's book" (I
suppose it was the Automath formlaization of Landau's Grundlagen der
Analysis by Jutting) which proves that "it can be done" but is
otherwise an intellectually barren exercise without academic value. I
still remember one of the professors saying this to the whole class
when was an undergraduate.

With kind regards,

Andrej