FOM: RE: Computer-verified theorems...IV

[Matt Insall]

Andrej:
In reality, software and hardware verification are big issues. The
computer industry is pouring millions of dollars into research on how
to detect and eliminate errors 1)--4) from the above list, whereas 5)
and 6) are completely irrelevant, except perhaps on airplanes and the
Space Shuttle.


Matt:
I would tend to disagree that 5) and 6) are irrelevant, in actuality.  The
inability to do something does not make it irrelevant.  Some way of
accounting for these things should, I think, be developed.  The reason I say
this is that all the things we do depend upon one another.  If we ignore 5)
and 6) in one context, and do not explicitly warn future users of our
results about the fact that we have not taken certain difficulties into
account, then we set them up for failure in what may be a critical
situation.  Now, I understand that mistakes may be made in determining
exactly what should be taken into consideration, but the nature of software
use is such that after a generation or two of development, certain things
are frequently presumed to work properly because so much has been put into
trying to be certain that they do.  Knowingly leaving out clear descriptions
of what has or has not been considered causes the industry to need constant
expensive revamping.  Now, perhaps pure mathematics can survive such
redundancies and false starts because pure mathematics is also a culture in
which there is constant scrutiny, and the most ``suspect'' results do not
get applied to potentially disastrous situations very quickly, but
technology is different.  When a need for a product presents itself, someone
develops it, according to some deadline, and it gets implemented, sometimes,
as we have seen in our society, over the objections of the developer.
Mathematical introspection has existed for centuries and has had some very
valuable consequences in mathematics and the sciences.  I suggest that the
software industry would benefit from even more careful attention to how
mathematicians deal with the expression of their ideas, both formally and
informally, and both syntactically and semantically.  It is clear that some
people in the industry understand this, just as it is clear that some do
not.



Matt Insall