Hi, On Tue, 26 Sep 2006, Freek Wiedijk wrote:
What is Georges Gonthier's language?It's the language that he developed on top of Coq for the formalization of the four color theorem. It's very compact and very nice. It's also very much not like Mizar (I remember Georges saying to me that he doesn't like the Mizar/Isar style of having a statement with each proof step; he thinks that that is completely the wrong approach; I don't think I agree, but I'm not 100% certain about that...)
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).
Quite interesting is also the regular naming scheme for theorems. I wish Mizar had something similar instead of those names like XREAL_1:74 .
Josef