from idea to project

LYBRHED@delphi.com
Date: Tue, 03 Aug 1993 04:00:34 -0400 (EDT)
From: LYBRHED@delphi.com
Subject: from idea to project
To: qed@mcs.anl.gov
Message-id: <01H1AMQV4V0O90NYL7@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

I have been reading "NeXTSTEP Programming:  Step One," by 
Garfinkel and Mahoney.  The two main projects in the book are... 
calculators!  First you build a little four-function calculator, then a 
more elaborate one that can graph functions.  I am struck by the 
fact that NeXTSTEP seems to be designed as a construction kit for 
making calculators.   And the idea of a "calculator" can be taken to 
whatever level of sophistication you want.  

Steve Jobs's original vision of the NeXT Cube could be described as 
"a platform for QED."   The original Cube came with Mathematica, 
Allegro Common Lisp, and  a built-in searchable digital library, at 
least in skeleton form.  It was a Pythagorean computer designed 
for mathematicians.  But so far the only mathematicians who 
have taken him up on it are the quants on Wall Street and the 
cryptographers at the CIA.  I don't think this was what Steve had 
in mind.    

In my last letter I said there should be a demo of QED, or actually 
a series of demos with increasing functionality.  Why not take the 
NeXT Cube as a prototype of QED?  Of course it fell far short of the 
ideal.  It was concerned with numerical calculations rather than 
proofs.  But it could be taken as a demo of Version 0 of QED.  It 
was a first approximation to "a computer system that contains all 
of mathematics."  It is the only computer that even aspires to be 
QED-like, and it actually exists, so it gives us a tangible starting 
point.

If the Cube is Version 0, then Version 1 would be a 486 computer 
running NeXTSTEP 3.x.  It will have a built-in proof constructor, to 
go with its built-in librarian and built-in calculation engine.  By 
"proof constructor" I mean a mathematician's workbench, 
something like the combination of editor, compiler, and debugger 
that programmers use.  It could be used to "compile" a proof into 
Machine Math and to connect it with other theorems in a 
"hypermath" network.  It would also be able to animate a proof, 
like the programs that animate sorting algorithms.  

Version 1 will also have at least the beginning of a mathematical 
library.  The Digital Librarian is already there in NeXTSTEP as a 
capability, but there is no actual content in the library;  at least 
no mathematical content.  The original Cube came with the works 
of Shakespeare on an optical disk.  Shakespeare was the whole 
library!  There is more in Heaven and Earth, Horatio, than is 
dreamt of in your philosophy!  This was where Steve's vision 
wavered.  This was one of his first strategic mistakes.  You have to 
give him credit for conceiving the idea of a computer with a built-
in library, but instead of Shakespeare he should have bundled a 
library of mathematical theorems, methods, and ideas.  Version 1 
of QED will have at least a token library, enough to see what it 
would look like.  

First it will be necessary to create the tools needed to write the 
proof constructor.  NeXTSTEP comes with "kits" for constructing 
various kinds of applications:  the Music Kit, the DB Kit, and so 
forth.  What we need is a Math Kit.  

This could be an actual project as soon as school starts in the fall.  
All we need to do is find some students who think working on 
Version 1 would be a good way to learn computer science and math 
at the same time, and at least one professor willing to teach them.