[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] A quote
On Mon, Jan 12, 2004 at 05:55:00PM +0100, Andrzej Trybulec wrote:
>
> 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" ?
I meant the rest of the section that started in p. 6, especially the mention
of things like: FTA or Reals in Coq, things that C. Simpson found worthwhile
mentioning while the same things have been done in Mizar if not earlier then
roughly at the same time.
I am attaching the entire letter that I sent to C. Simpson but have not
heard anything in reply.
--
Piotr Rudnicki CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr
-----------------------------------------------------------------------------