From idea to project
LYBRHED@delphi.com
Date: Fri, 06 Aug 1993 01:10:43 -0400 (EDT)
From: LYBRHED@delphi.com
Subject: From idea to project
To: qed@mcs.anl.gov
Message-id: <01H1ENP1D8ZS91XAWH@delphi.com>
X-Vms-To: INTERNET"qed@mcs.anl.gov"
Mime-Version: 1.0
Content-Type: TEXT/PLAIN; CHARSET=US-ASCII
Content-Transfer-Encoding: 7BIT
Sender: qed-owner
First I want to correct a mistake that has been bothering me for a
month. In "Objection 10" I misspelled Stuart Kauffman's name.
Two f's, one n. I am the kind of perfectionist who actually worries
about such things.
Now, about turning QED into a project: Back at the beginning of
this discussion, David McAllester said that he could write a simple
routine that would translate definitions and theorems from any of
the other theorem-proving languages into Ontic. Nobody said "All
right, let's do it."
A few days later Michael Beeson came up with some excellent
suggestions for making QED into a project, but no one said "Ok, let's
do it."
Then several people suggested getting students involved; make QED
part of the cs curriculum, and get students to do much of the
work. Once again, no one said "Ok, let's do it."
I have a sense of futility about this. No matter what we suggest,
nothing is going to happen.
About portability: eventually the mathematics library will reside
somewhere out here on the Net. You will be able to access it with
just about any kind of computer. But that is several years in the
future.
When we make a prototype system, at some point somebody is
going to have to sit down and start writing code in a specific
language on a specific computer. At that stage it will not be
portable.
Lyle