Re: [mizar] Private DB

[Freek Wiedijk <freek@cs.ru.nl>]

Hi Josef,

>I agree that there should be a mechanism for deciding what is "the real 
>Mizar", and also think that the current practice of having Andrzej (and 
>Czeslaw) do that is not bad. But I (obviously) strongly disagree with 
>preventing people to experiment with Mizar and "diverge" from it.

But!  In the case of Isabelle and HOL Light (or for instance
Andrea Asperti's Matita as a "divergence" from Coq), those
really are not branches of an older system!  Those are totally
new systems, very much inspired by the old one, yes, but _not_
a derivative.

If you would go, and build a system that very much resembles
Mizar but is a "new" system really, then I wouldn't complain
about it at all.  (And if you do this, _please_ allow empty
types: Mizar is _evil_ that it doesn't allow empty types :-))

In the case of Georges Gonthier's language (which I do indeed
like very much), you're kind of right.  But really it's _not_
well integrated into Coq-as-a-system, I think.  It's really a
layer on top of it.

Freek