Re: [mizar] be and being

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

Josef:

>You may be right, but concerning these writability/readability problems, I 
>would be quite careful.
>The next steps in this direction might be suggesting something like 
>"!" instead of "for", "?" instead of "ex", "~" instead of "not", or even 
>things like "Intro;" instead of all the initial "let" and "assume", etc.
>
>These certainly improve writability, but Mizar might end up being as 
>readable as some other systems - have a look at the comparison texts 
>collected by Freek at http://www.cs.kun.nl/~freek/comparison/index.html.

So I made a "Mizar mode" for HOL called Mizar Light, and also
Mariusz Giero recently has made a Mizar mode called "MMode"
for Coq.  In those systems, one uses the Mizar notation for
the proof steps but HOL or Coq notation for the formulas.

My experience is that proofs that use these "modes" are very
"Mizar like", and pretty understandable.

But when I tried to play my "formal proof sketch" game
(making a Mizar proof with possible "*4 holes" in it look as
much as possible to some already existing informal proof from
the literature) with my Mizar Light mode for HOL, it did not
work _at all_ as well as when I did it with the real Mizar.

Freek