Re: [mizar] Private DB

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

Hi Josef,

>At least from his description 
>(http://research.microsoft.com/~gonthier/4colnotations.pdf) it seems that 
>sometimes he chooses to be more declarative than Coq (but I have not 
>looked at the actual code).

Yes, he looks at it like that, and in a sense he's right, in
his language many more things are explicitly present "in the
script" than is the case when you use vanilla Coq.  But
really, the way I look at it is that his system is the
ultimate refinement of the _procedural_ style of formal proof.
It's really about tactics transforming a goal.  And because
his tactics are so powerful, they change the goal _a lot_ at
every step.

Maybe the way one uses Georges Gonthier's system is like I saw
Jeremy Avigad use Isabelle/Isar.  One does the "human level"
steps declaratively, and then hack the intermediate steps that
link them together in a procedural way.  Who knows, maybe
that's the best way to do formalizations.  I don't know.

>Quite interesting is also the regular naming scheme for theorems.

I didn't know about this, I'll look at the paper.  Thanks for
mentioning this.

Freek