Delivery-Date: 
Message-Id: <0iG1wi2KmlE508BWc0@earth>
Date: Wed, 10 Aug 1994 10:28:30 +1000 (EST)
From: Zdzislaw Meglicki <Zdzislaw.Meglicki@cisr.anu.edu.au>
To: qed@mcs.anl.gov
Subject: Re: Types Considered Harmful
In-Reply-To: <9408090532.AA18788@maui.cs.ucla.edu>
References: <9408090532.AA18788@maui.cs.ucla.edu>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

> The debate of whether one should use set theory or type theory sounds to
> me a bit like the debate of whether one should use C or Pascal.

No, it's like the debate whether one should write piano concertos in C
or in E-flat. But... when you sit in front of an empty sheet of paper
about to begin writing a concerto, you must make this decision before
you can do anything else. And once you've made it, you've got to stick
to it. 

Because writing a QED system is a far more elaborate task than writing a
piano concerto, and many more people would be involved, a good decision
is that much more difficult to make.

If you ask about the "usefulness" of the whole project and wonder if any
commercial company would be willing to pay money for it, the answer is:
"possibly". Vendors of "Mathematica", "Maple", and other similar
software systems make quite good living by selling computerised
mathematical encyclopedias and symbol manipulation environments. They
might  be interested in QED - at least to the extent to which it could
be utilised in their own products. By the same token, software and
hardware vendors interested in formal verification of their products
might also be willing to support QED.

   Zdzislaw Meglicki, Zdzislaw.Meglicki@cisr.anu.edu.au,
   Automated Reasoning Pursuit - CISR, and Plasma Theory Group - RSPhysSE,
   The Australian National University, Canberra, A.C.T., 0200,
   Australia, fax: +61-6-249-0747, tel: +61-6-249-0158