Re: Hardware Verification and New Mathematics

cal@ANTARES.AERO.ORG
Tue, 22 Nov 1994 10:13:49 -0800

I have been following the recent discussions about verifying chips with some
interest, and it seems to be about time to raise one interesting aspect of the
discussion. Those people who say that we have made great strides (which I
agree with, BTW) all write about advances in the engineering and modeling
aspects of the problem. Nobody so far has noted that there is another avenue
of possible improvement, namely, in the underlying Mathematics. It is
problems like this one in hardware verification, in which we can do some
things quite well, but the "real" existing problems are still too complex,
that stimulated us to begin our New Mathemtical Foundations for Computer
Science initiative. I have enclosed the current issue of the Workbook, which
has references to more information.

Simply put, as a modeler, I want new Mathematical tools to use for my models.

more later,
cal

New Mathematical Foundations for Computer Science

Workbook Edition 1.2: More Abstracts, On-line Conference, MUD
(Last Modified: 23 October 1994)

Editorial Contacts:

Dr. Christopher Landauer
System Planning and Development Division, The Aerospace Corporation
The Hallmark Building, Suite 187
13873 Park Center Road, Herndon, Virginia 22071
e-mail: cal@aero.org
Phone: (703) 318-1666, FAX: (703) 318-5409

Dr. Kirstie L. Bellman
ARPA / SISTO
3701 N. Fairfax Dr.
Arlington, Virginia 22203
e-mail: kbellman@arpa.mil
Phone: (703) 696-2219, FAX: (703) 696-2202

Abstract:

This Workbook is the record of a continuing online conference on New
Mathematical Foundations for Computer Science. We intend to collect and
redistribute varyingly formal contributions about this topic area. We expect
that the contributors will collectively develop some interesting ideas that
will become an edited book of more formal articles.

Our intention with this initiative is to promote the notion that part of the
reason for the repeated failure of large computing systems is that we (in this
culture) have reached the end of a paradigm in computing, and that we need
more and different mathematics, indeed a new theoretical foundation for the
science of computing, in order to proceed. The focus of this initiative is the
nature of that new mathematics that might be important in a new foundation for
computing.

History:

Because of the surprisingly interested responses we have had to our informal
conversations over the last year or so, we decided to make them more public by
starting an online, continuing, distributed workshop to allow open discussion
of the issues and ideas. The Questions under discussion are:

1. Why is it so hard to analyze, construct or change large, heterogeneous systems?
Our answer is that we have reached the end of our paradigm.
2. Do we need new mathematical foundations for these new kinds of computing?
Our answer is a simple YES.
3. What is (the nature of) the new Mathematics that is needed for Computing?
This is the main focus of the Workbook.
4. What are some interesting new applications of existing mathematics,
especially in the newer areas of theoretical and applied computing (e.g.,
concurrency, interaction, collaborative systems, building complex systems,
...)?
LOTS, we think. This is the second focus of the Workbook.
5. ... <your problem or question here> ... -
We _know_ there are more good questions out there.

Invitation:

I would be pleased to include in the Workbook an abstract, technical paper, or
position paper that contributes to these questions. Feel free to invite anyone
you know who might have something interesting to tell us to contribute to it.
Please submit all contributions electronically to C. Landauer:

cal@aero.org

(I can also handle uuencoded compressed files, with compress or gzip).

Process:

After I have looked at a submitted abstract, it will appear in a directory
accessible via anonymous ftp at:

aerospace.aero.org

in a directory under

/pub/newmath

I will include submissions in the table of contents in the order in which I
receive them; I prefer postscript files for the abstracts and papers, and will
certainly accept ASCII text files.

I have no facilities for redistributing paper.

Legal Stuff:

Each submitter retains copyright, but by submitting explicitly gives
permission for unlimited redistribution without change and without charge, as
long as the source information is included (e.g., the author and author's
e-mail address or source site, and possibly also reference to the New Math
workbook). We _want_ people to copy and circulate these abstracts and
discussions and read them.

Organization:

There are several directories under the newmath directory at the ftp site,
with README or TWIMC (To Whom It May Concern) files in each. At present, there
are directories "imacs" for the IMACS conference information (see the initial
workbook file "workbook940718.txt" for a description of the conference),
"abstracts" for abstracts and papers not from the IMACS session, and two
currently empty ones for e-mail discussions ("mail") and logged MUD
conversations ("mud").

The current organizational setup has the ftp site listed above, a very
generously provided Web home page (thanx to Professor Ashok Agrawala) at the
University of Maryland:

http://www.cs.umd.edu/~agrawala/newmath.html,

and a discussion area on DragonMUD (a Multi-User Domain; text-based virtual
reality) for technical conversations in a Virtual Place (DragonMUD is located
at tinylondon.ucsd.edu 4201).

The distributed online conference will eventually include directories in the
current ftp archive for abstracts, papers and discussions, references to other
ftp archives for longer papers, a sensibly cross-referenced (probably using
HTML files) collection of topical discussions, a mailing list for those
discussions, reviews and commentary of articles and abstracts (also
cross-referenced and Web accessible), logs of the technical conversations that
are held on DragonMUD, and announcements of relevant conferences and other
activities of interest. Anyone who would like to help me set this up should
please let me know (same e-mail address).

Workbook Table of Contents:

workbook941023.txt (this file)
Introduction to Workbook (Edition 1.2)
C. Landauer
workbook940718.txt (original version, 18 July 1994)
Introduction to Workbook (Edition 0)
C. Landauer
imacs/imacs-session.txt.Z
IMACS Conference Session Announcement
C. Landauer
imacs/cal-imacs.txt.Z
imacs/vg-cal-imacs.txt.Z (viewgraphs, text form)
imacs/vg-cal-imacs.ps.Z (viewgraphs, postscript form)
New Mathematics for Computing - What?
Christopher Landauer cal@aero.org
Kirstie L. Bellman kbellman@arpa.mil
imacs/clt-imacs.ps.Z
imacs/vg-clt-imacs.ps.Z (viewgraphs)
Mathematical Foundations for Survivable Systems
Carolyn Talcott clt@sail.stanford.edu
imacs/vijay-imacs.ps.Z
Mathematics on the Interface: Towards Adaptive Engineered Systems
Vijay Saraswat saraswat@parc.xerox.com
Daniel Bobrow bobrow@parc.xerox.com
imacs/don-imacs.txt.Z
Non-Platonic Integers
Don Walter dwalter@physci.ucla.edu
imacs/jose-imacs.ps.Z
Formal Interoperability
Jose' Meseguer meseguer@csl.sri.com
abstracts/herlihy.ps.Z
Applications of Algebraic Topology to Concurrent Computation
Maurice Herlihy herlihy@crl.dec.com
Nir Shavit shanir@math.tau.ac.il
abstracts/multimedia.ps
Formal Methods and Multimedia
Paul Hudak hudak-paul@cs.yale.edu

Last Modified 23 October 1994