Freek,
I never heard a serious explanation of why the sources are closed,I know two anecdotes related to this (but maybe for you neither of them is serious):
Right, they are anecdotes, and they are always told in that spirit. Problem is that in eight years I really never heard any _serious_ argument, to say nothing about having a serious and rational discussion. Nothing to match the arguments expressed in the couple of previous e-mails, and told over and over in many other places (read e.g. the last-but-one paragraph of http://www.dwheeler.com/essays/high-assurance-floss.html).
- The current policy of only getting the sources when you write at least one serious Mizar article made _you_ write some very nice Mizar articles. So that policy payed off.
No, I can't see how anyone can claim that because I (or someone else) was forced to write one Mizar article, the policy paid off. That does not account for the damage this policy causes. For my Msc. work, I originally rejected Mizar right in the beginning, because I could not easily get its source. Then it took at least a year of useless workarounds before I was forced by my PhD supervisor to write the article so that I could get the sources. I would probably never decide to do this myself, and rather turned to other open-source proof assistants (I was experimenting with IMPS a lot at that time).
There were other people since, who struggled with reverse engineering Mizar (without writing any article), and also others who rejected Mizar because of non-openness. Obviously those who rejected it immediately are a bit hard to count :-).
- The sources used to be open, but then the only effect of that was that some silly person made a version of Mizar that just was different in that all the keywords had been changed. That was so irritating that after that the sources got closed.
I can't see what is irritating about thousands versions of Linux kernel being used by various people. Some of the patches will never be accepted into "official Linux" by Torvals/Morton, some will, some will get strong support from their users anyway. There are countless examples of this - the year is now 2008, not 1980 :-). One of them is obviously all the various flavours of HOL and Isabelle. It is a fairly speculative subject, but AFAIK this diversity and parallelism has rather fostered the development of HOL-based systems than not (think e.g. Isar vs. old-style Isabelle, Meson vs. Metis vs. Sledgehammer, the cool HTML presentation for Isabelle/ZF at http://formalmath.tiddlyspot.com/, etc.).
Also, last time I heard that someone in Germany did translate Mizar-MSE keywords to German, it was in Bialystok, and accepted positively.
Josef