[FOM] 187:Grand Unification 2 - saving human lives
Harvey Friedman
friedman at math.ohio-state.edu
Wed Jul 2 10:39:44 EDT 2003
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
More information about the FOM
mailing list