[FOM] 187:Grand Unification 2 - saving human lives

[Harvey Friedman]

This is a continuation of posting #186, and puts the proof checking 
project into a wider perspective.

Recall that in #186, I outlined a GRAND UNIFICATION project, calling 
for the development of efficient decision procedures for finite 
languages of short assertions surrounding basic mathematical 
contexts. This represents a paradigm shift for mathematical logic, 
involving at least tameness issues, elementary proof theory, decision 
procedures, algorithm design and implementation, language design, and 
also, at least projected down the road, set theory and large 
cardinals. There are both deep foundational and practical motivations 
for this development.

There is a vitally important project that has only gotten off the 
ground in limited ways in rather specialized hardware contexts. E.g., 
Intel and IBM have or have had projects involving the formal 
verification of aspects of chip design - especially arithmetic 
circuit design - which are specified by the IEEE arithmetic standards.

DESIGN AN APPROPRIATE LANGUAGE FOR SOFTWARE DEVELOPMENT WHICH 
SUPPORTS FRIENDLY DEVELOPMENT OF EFFICIENT CODE THAT IS SPECIFIED AND 
VERIFIED AS PROGRAMS ARE BEING DEVELOPED.

So here we are talking about verifying proofs that programs are 
correct as they are being developed.

This is hopeless for anything like general purpose software given the 
programming techniques currently in use.

What is needed is an appropriate mathematically friendly functional 
programming language, with clear mathematically friendly semantics, 
which does not sacrifice much in the way of efficiency. Complete 
modularity, no side effects, where semantics is inherited from the 
standard semantics of mathematics, etc. It should be noted that there 
are plenty of important contexts in which efficiency is not even 
remotely at issue but correctness and specification is - for example, 
in the area of the design and implementation of complex user 
interfaces.

Current complex software is almost certainly all BUGGY. Furthermore, 
in looking, say, at military applications - e.g, in the recent wars - 
we see a suspiciously frequent number of deadly mistakes. One can 
only speculate that some of this is due to BUGGY SOFTWARE.

I have no doubt that major decisive breakthroughs await us in coming 
years on this project, and the effectiveness of it will depend on at 
least having first developed truly workable user friendly proof 
verification systems, well before one combines this effectively with 
the badly needed PROGRAMMING LANGUAGE REDESIGN.

Hence the yet additional importance of what was discussed in Grand 
Unification 1, posting #186.

Most people didn't go into foundations of mathematics in order to 
SAVE HUMAN LIVES, but this may be a very natural and inevitable 
ultimate outcome of their efforts.

*********************************************

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 187th in a series of self contained numbered postings to 
FOM covering a wide range of topics in f.o.m. The list of previous 
numbered postings #1-149 can be found at 
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html  in the FOM 
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms, 4/22/0  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM
174:Directly Honest Second Incompleteness  6/3/03  1:39PM
175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM
176:Count Arithmetic  6/10/03  8:54AM
177:Strict Reverse Mathematics 1  6/10/03  8:27PM
178:Diophantine Shift Sequences  6/14/03  6:34PM
179:Polynomial Shift Sequences/Correction  6/15/03  2:24PM
180:Provable Functions of PA  6/16/03  12:42AM
181:Strict Reverse Mathematics 2:06/19/03  2:06AM
182:Ideas in Proof Checking 1  6/21/03 10:50PM
183:Ideas in Proof Checking 2  6/22/03  5:48PM
184:Ideas in Proof Checking 3  6/23/03  5:58PM
185:Ideas in Proof Checking 4  6/25/03  3:25AM
186:Grand Unification 1

Harvey Friedman