[FOM] Schwartz on verification
Harvey Friedman
friedman at math.ohio-state.edu
Thu Jul 3 16:08:25 EDT 2003
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
More information about the FOM
mailing list