Why Mathematical System Modeling Needs the Mathematics of Analysis

Konrad Slind <slind@informatik.tu-muenchen.de>
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: boyer@CLI.COM
Cc: qed@mcs.anl.gov
In-Reply-To: <qed-owner@mcs.anl.gov>'s message of Fri, 23 Apr 1993 05:35:40 +0200 <9304230335.AA19436@axiom.CLI.COM>
Subject: Why Mathematical System Modeling Needs the Mathematics of Analysis
Message-id: <93Apr24.004720met_dst.8079@sunbroy14.informatik.tu-muenchen.de>
Date: 	Sat, 24 Apr 1993 00:47:11 +0200
Sender: qed-owner
Precedence: bulk


Robert S. Boyer writes

> Currently software and hardware proving is very introspective,
> focusing upon compilers, operating systems, multipliers and such.  We
> rarely more than dream about mechanically checking theorems about
> applications that interact with the continuous world, the very world
> that was the inspiration for analysis, the world in which safety
> critical systems are at risk of doing their damage.  I believe that we
> don't yet study such applications because it seems so hard, perhaps
> impossibly hard to do all by oneself from scratch.

I don't agree. One reason why we have not got on to verifications of
continuous/discrete systems is that the verification of devices having
arithmetic or even purely logical specifications is still quite
fruitful, in terms of successes and of research interest. Of course,
verifications utilizing more complex models are important challenges
still confronting the field (see below).

> I believe it would immensely help the prospects for beginning to treat
> the mathematics of computer systems that interact with the continuous
> world if there existed a rigorous, substantial body of mechanically
> checked formal definitions and theorems about integrals, partial
> differential equations, and the rest of mathematics used by engineers.

There are already significant theories of the real numbers in, at least,
the HOL, IMPS, and Nuprl systems. Of course, these are but a fraction of
the massive amount of analysis that has been done on paper and in
computer algebra systems, but we certainly don't need to wait for QED to
come to fruition in order to start verifying systems specified in terms
of the reals. As a byproduct of such verifications, these theories can
only become deepened and extended, thus acheiving many of the goals of
QED in a relatively quiet and simple manner.

Konrad.