Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Posted-Date: Fri, 8 Apr 94 07:04:10 PDT
Message-Id: <199404081404.AA01265@aerospace.aero.org>
Date: Fri, 8 Apr 94 07:04:10 PDT
From: cal@aero.org
To: info-hol@leopard.cs.byu.edu
Subject: Re: How close is practical program proving? AND MORE
Cc: cal@aero.org


Peter Homeier (HI, Peter!) asked how soon we could buy verification products
for programming languages - and, more interestingly (to me), he asked what
makes program proving so hard -

Jim Grundy gave an interesting and helpful discussion about the problem,
mentioning some partial formalizations -

There are LOTS of formalizations of parts of programming languages - the
problem seems to be that every programming language is a compromise between
formalizable theory and electronic behavior, and in case of conflict,
electronics wins

- and some good comments on things that are hard to program, and some
suggestions for how to write a program that is intended to be proved -

so I think that part of the problem is the nature of the programming languages
currently in use - they are still relics of old assumptions about the nature
of computing - for example, explicit input and output statements are a
historical artifact that result from old hardware designs that made knowing
when your program or data was in core important - with modern paging, you
almost never know - so they should all be changed to persistent or volatile or
stream variables and assignments, and let the OS keep track of where they are
... (more philosophy later)

Ching Tsun's question about which programs are worth proving implicitly
assumes that program proving is very hard (otherwise, it would not be an
interesting question) - but why should this be true?

but nobody said anything about

	how we write a specification in the first place
	(i.e., what are we going to prove anyway?)

	how paltry the mathematics is that supports this kind of analysis
	(though Jim did mention the lack of simple mathematical models,
	which is on the right track - i believe even more: that there isn't
	even any sufficiently powerful mathematics to use for such models)

which brings me to the "AND MORE" part of the message -

IMACS Announcement - please distribute to interested parties

The 14th IMACS World Congress is in Atlanta next July 11-15 (IMACS = Int.
Assoc. for Mathematics and Computers in Simulation).  I have organized a
session on ``New Mathematics for Computing'' (see my proposal to the
conference organizers below), which includes papers on context and
self-reference, other new logics, and a few other topics I find interesting.
I have some thoughtful people from the mathematics, computing and artifial
intelligence communities who will speculate interestingly about what new
mathematics might be needed for computing.

	THE SESSION IS FRIDAY AFTERNOON, July 15, 2:15-5:15pm
	(for more detailed conference information, see below)

The reason for the session is to start discussions and announce our interest
to the rest of the research community.  The session will therefore contain
more speculative notions and research problems than solutions, though a few
promising or successful directions are included.

In particular (just to give you an idea of my own prejudices), I think that
the area of computational complexity is not helpful in the way I want, since
asymptotics are not the main problem; the constants needed for the mid-range
(very large but not infinitely large values) are.

I am especially interested in the kinds of computing problems people think the
research community has skipped or deferred because they are too inelegant or
otherwise strange (heterogeneity is an important property of complex systems).
I want to make this session an announcement to all mathematicians and "fellow
travelers" that we need more models, methods, concepts, and formal spaces in
which to do interesting things if we are to study complex systems effectively.

Session Proposal for IMACS

Title: New Mathematics for Computing

There is no existing mathematics that can adequately describe some of the new
computational paradigms now in widespread use in software for complex systems
involving computers, and it is even harder to give a formal basis for hybrid
combinations among these new paradigms.  This session will focus on the new
kinds of mathematics that these systems seem to require, and on some promising
lines of research in mathematics and computation.

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

The Conference organizer is

William F. Ames
School of Mathematics
Georgia Institute of Technology
Atlanta, Georgia 30332-0160
(404) 894-3953

ames@math.gatech.edu