Re: [mizar] Private DB

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

Hi Jesse,

>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...)  Georges language is
very "perl like" in the sense that lots of things are made to
happen with little flags that modify and extend the command.
Because of this there are only a small number of tactics
needed for the majority of the proof.

You can see a small example of Georges language by going to
the end of <http://www.cs.ru.nl/~freek/demos/>.  There you can
also find links to Georges' home page (on which there is a
document that explains the language, I think), and to the page
of his institute (the joint Microsoft-INRIA "labo".)

Freek