Re: [mizar] Hindrances

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Freek:

I understand your concern and I also think that the role of MML in
policing the authors should be minimal.  Yet, there are many obvious
cases where the current state of MML literally is hindering rather
than helping the authors and the MML development.  This is why Andrzej
uses the term "hindrances."  In our MKM paper (preliminary version is
at http://www.cs.ualberta.ca/~piotr/03ATMKM/) we gave numerous
examples of what kind of "hindrances" we had in mind. There is no
general theory of what a hindrance is, we are looking for such
hindrances where a concensus can be reached.  If anyone has comments
on the hindrances discussed in the paper, this forum would be a good
place to discuss them.

Greetings,

PR


PS Some 25 years ago I was planning to write a short satire on the entire 
   formalized mathematics database but I did not get far past the title,
   and the tilte was "MathPol".


On Fri, Nov 08, 2002 at 09:43:12PM +0100, Freek Wiedijk wrote:
> Piotr,
> 
> >Does anyone have a better idea how to name issue that
> >Andrzej describes below
> 
> In a sense it's about removing choices.  That when you write
> a Mizar article there's only one "right" way to write it.
> 
> But in a way I don't like that: because what if I don't like
> the "right" way, and want to write things the way that
> pleases me?  Then the MML will work against me!
> 
> Freek

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr