Re: [mizar] A quote

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Piotr Rudnicki wrote:

>
>         +<http://xxx.lanl.gov/ps/math.HO/0311260>ps,

>
> One may not agree with the above (especially in the light of the rest of the
> paper).  However, it is inevitable that people will be discouraged by the
> amount of garbage in MML.  In this light the "weak types" can wait.

Piotrek,

I have read the paper and I rather like it. Particularly p.17 (section 'Exotic versus regulat math'):

  So there are undoubtedly lots of fun things to look at in these exotic
reaches, but they don't really have anything to do with our original goal
of implementing, as quickly as possible, a large amount of standard mathe-
matics. More generally, my experience is that any "brilliant gadget" seems
predestined to be a bad idea. Boring as it may seem, we have just to plod
along in a mudane but systematic way.

I completely agree with Carlos Simpson.

What you mean by "especially in the light of the rest of the
paper" ?

The best,
Andrzej