On Wed, 7 Nov 2007, Freek Wiedijk wrote:
_Some_ people would say that if only Mizar were open source, this might not be a problem, but I don't agree with that. (The Coq source _is_ open, and there are only a few who can modify that code as well. I think.)
It really feels like the autumn discussion season has arrived to Nijmegen :-). One fresh comment on this evergreen is that even the evil capitalist US are considering a bill making results of publicly funded research mandatorily openly available (http://www.nature.com/news/2007/071107/full/450148a.html).
Josef