Re: Continuing Conversation - NO Flames

• Mail folder: QED
• Next message: Larry Wos: "another country"
• Previous message: cal@aero.org: "Continuing Conversation - NO Flames"
• Maybe in reply to: cal@aero.org: "Continuing Conversation - NO Flames"

Message-id: <8fu5Bt_KmlE2BHIGot@arp>
Date: Thu,  6 May 1993 09:53:29 +1000 (EST)
From: Zdzislaw Meglicki <Zdzislaw.Meglicki@arp.anu.edu.au>
To: qed@mcs.anl.gov
Subject: Re: Continuing Conversation - NO Flames
Sender: qed-owner
Precedence: bulk

In <199305051835.AA02457@aerospace.aero.org> cal@aero.org writes:

> My note about failures of imagination was not intended to imply ineptness;
> only that we are up against a very hard problem, and we need even more smarts
> about abstraction than the kinds currently in use.

This is where the challenge for a system such as QED is. If only 
currently available techniques and technology were sufficient then where
would the  challenge be? It would merely be just a bureaucratic exercise
in translating a book or a collection of books into a computer code. As
QED develops I am sure that great many insights and new techniques will
be developed. The richness of mathematics will force QED implementors to
do just that. It is a bit like with the landing on the Moon. When JFK
made his famous speech the technology to achieve that didn't exist yet.
But to set up the goal provided the impetus for further technology
developments and ultimately we all ended up having microwave ovens and
teflon frying pans in our kitchens. Can you imagine life without a
microwave? In 20 years time engineers will find it equally hard to
believe that once upon a time people were doing mathematics without QED!

   Zdzislaw Gustav Meglicki, gustav@arp.anu.edu.au,
   Automated Reasoning Program - CISR, and Plasma Theory Group - RSPhysS,
   The Australian National University, G.P.O. Box 4, Canberra, A.C.T., 2601, 
   Australia, fax: (Australia)-6-249-0747, tel: (Australia)-6-249-0158