Re: [mizar] be and being

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Dear prof. Rudnicki,

On Tue, 16 Dec 2003, Piotr Rudnicki wrote:

> Therefore I propose that both 'be' and 'being' have an alias ':'
> which is shorter and commonly used in this context in everyday
> writing, not to mention some other system that use it.

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.

I think Mizar should (try to) be readable by normal mathematicians (all 
those talks about mathematical vernacular), not just specialized 
formalizers, and e.g. the recent shift in Isabelle towards Isar is also in 
the direction of much better readability (inspired by Mizar).

The writability can be improved by all kinds of external tools - I 
recently did the skeletons in Emacs, maybe Mizar could even be fully 
embedded as a "core language" into some other related systems that 
support more automation (e.g. Isabelle or PVS come to mind).


Best,
Josef