[FOM] Schwartz on verification

[Harvey Friedman]

Professor Jack Schwartz of the NYU Courant Institute, mathematician 
and computer scientist, has kindly written me the following valuable 
information regarding a research project he has been involved with 
for some time, which shares some of the same philosophy as I 
described in my recent postings on formal verification, automated 
proof checking, Grand  Unification, etc.

He has given me permission to post his letter on the FOM.

Schwartz et al have taken a focused set theoretic approach to 
programming and related issues in verification, through the set 
theoretic programming language SETL. A lot of detailed work has been 
done by them on practical decision procedures concerning fragments of 
set theory to support SETL and the verification of programs in SETL.

Without having studied this work sufficiently carefully, I would like 
to make some remarks.

1. The subject of decision procedures for fragments of mathematics is 
incredibly vast, and the contexts are incredibly varied, that one can 
look to the future for an enormously expanded multidimensional 
development.

2. The ultimate goals that I described need to incorporate, from the 
outset, at least, a fully functional approach with undefined terms 
and various related and additional standard mathematical devices, of 
course combined with standard set theoretic mechanisms, that is so 
characteristic of mathematical practice.

3. The expansion of the basic setup from a primarily set theoretic 
paradigm to one that is much more sensitive to actual mathematical 
practice and also the most natural implementation of algorithms, 
creates a number of delicate implementational issues concerning 
efficiency, as well as whole new universes of  relevant decision 
problems involving whole new universes of carefully chosen (finite) 
language fragments.

4. Undoubtedly, Schwartz et al will disagree with at least some of 
2,3 above. However, I think that they will agree that we are still 
very far from the ultimate goals I set out in my recent postings. The 
issue of extreme natural friendliness is absolutely critical for the 
largely universal adoption that would really be needed to drive the 
impending revolution.

Harvey Friedman

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

Dear Prof Friedman:

Martin Davis,  my friend of  many decades, just now made me aware of 
your series of postings on the email list
FOM "foundations or mathematics". I have so far only had time to 
scan them very hurriedly. But I note  that the
GRAND UNIFICATION project which you advocate in your #186 and#187 
(Wed Jul 2), as represented by your remark

"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."

seems to lie  close to a program, first theoretical (decision 
algorithms for small sublanguages of mathematics) and more lately 
practical, (but alas still only partially complete) of building an 
actual verifier. that I have been pursuing for some time with a group 
of collaborators,most at the University of Catania.

Much of this is described in our partial draft book, 'A 
set-theoretically based proof verifier and its application to the 
basic theorems of analysis', which you can find online (in its 
'as-is' state) at
<http://www.settheory.com/intro.html>A set-theoretically based proof 
verifier and its application to the basic theorems of analysis. Among 
other things, this describes a partly complete verifier, written 
(much as you seem to advocate) in a set-theoretic programming 
language (called SETL) (described at 
<http://www.settheory.com/>http://www.settheory.com/), Detailed and 
partly verified definition and proof  scenarios acceptable to this 
verifier have so far been built  up for part of what might be called 
the 'von Neumann-Landau' path leading from the basics of set theory 
to our stated goal, the Cauchy integral theorem. We have gotten as 
far as partial verification of most of the basic properties of the 
real numbers, defined as Dedekind cuts.

This attempt in progress was preceded by a lengthy period of work on 
decision algorithms for various sublanguages of set theory and 
analysis, as e.g. the early

Decision Procedures for Elementary Sublanguages of Set Theory

Part I: Multi-Level Syllogistic and its Extensions (with A. Ferro and 
E. Omodeo), Comm. Pure and Appl. Math., vol. 33, pp. 599-608, 1980.

Part II: A Decidable Class of Quantified Formulae (with A. Ferro, M. 
Breban and E. Omodeo), Comm. Pure and Appl. Math., vol. 34, pp. 
177-195,1981.

Part V: Multilevel Syllogistic Extended by the General Union 
Operator, (with D. Cantone and A. Ferro), J. Comp. System Sciences, 
vol. 34, pp. 1-18, 1987.

Part VI: Multilevel Syllogistic Extended by the Powerset Operator, 
(with D. Cantone and A. Ferro), Comm. Pure Appl. Math., vol. 38, pp. 
549-571, 1985.

recently much extended and comprehensively reviewed in 
<http://www.amazon.com/exec/obidos/tg/detail/-/0387951970/qid=1057234996/sr=1-1/ref=sr_1_1/002-6953866-8552828?v=glance&s=books>Set 
Theory for Computing: From Decision Procedures to Logic (Domenico 
Cantone, Eugenio Omodeo, Alberto Policriti ) and

  <http://www.amazon.com/exec/obidos/tg/detail/-/0198538073/qid=1057235205/sr=1-2/ref=sr_1_2/002-6953866-8552828?v=glance&s=books>Computable 
Set Theory  (by Domenico Cantone, Alfredo Ferro, Eugenio 
Omodeo,)<http://www.amazon.com/exec/obidos/tg/detail/-/0198538073/qid=1057235205/sr=1-2/ref=sr_1_2/002-6953866-8552828?v=glance&s=books>

Jack Schwartz
Courant Inst.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: /pipermail/fom/attachments/20030703/95e40a89/attachment.html