Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 23 Apr 1993 05:38:34 +0100 Received: by antares.mcs.anl.gov id AA07009 (5.65c/IDA-1.4.4 for qed-outgoing); Thu, 22 Apr 1993 22:36:06 -0500 Received: from cli.com by antares.mcs.anl.gov with SMTP id AA06994 (5.65c/IDA-1.4.4 for ); Thu, 22 Apr 1993 22:35:58 -0500 Received: by CLI.COM (4.1/1); Thu, 22 Apr 93 22:30:11 CDT Date: Thu, 22 Apr 93 22:35:40 CDT From: Robert "S." Boyer Message-Id: <9304230335.AA19436@axiom.CLI.COM> Received: by axiom.CLI.COM (4.1/CLI-1.2) id AA19436; Thu, 22 Apr 93 22:35:40 CDT To: qed@mcs.anl.gov Subject: Why Mathematical System Modeling Needs the Mathematics of Analysis Reply-To: boyer@CLI.COM Sender: qed-owner@mcs.anl.gov Precedence: bulk Perhaps Konrad Slind is identifying what is desired with what is currently feasible when he asserts: Specifications of computer systems often draw very little from conventional mathematical knowledge of the sort that QED is aimed at codifying. The true purpose of a computer flight control system is to help keep an airplane from crashing while getting it where it should go. But it is currently right at the edge of the state of the art in mechanical proof-checking to prove in a really rigorous way, from first principles, such as the definition of sine, convergent series, etc., something like: The sine of .5 is within 1/645120 of 1841/3840. No one, to my knowledge, in the business of mechanical program proving has begun to deal with anything like the equations of aerodynamics, which presumably are part of the basis from which engineers deduce what flight control code will do. As far as I know, it would be a major advance today to prove theorems mechanically about a computer device as simple as a modem, right at the interface between digital and continuous signals. 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 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. Bob