Re: Ariane 5 failure

[dewar@merv.cs.nyu.edu (Robert Dewar)]

Matthew says

"Believe me, I would love to write a software system that I knew were
(formally) correct and didn't require run-time checks.  But I am not able
to build that system today.  So what should I do?"


First of all, I would object to the "formally" and even the word "corect"
here. These are technical terms which relate to, but are not identical with,
the impoortant concept which is reliability.

It *is* possible to write reliable programs, though it is expensive. If you
need to do this, and are not able to do it, then the answer is to investigate
the tools that make this possible, and understand the necessary investment
(which is alarmingly high). Some of these tools are related to correctness,
but that's not the main focus. There are reliable incorect programs and
correct unreliable programs, and what we are interested in is reliability.

For an example of toolsets that help achieve this aim, take a look at the
Praxis tools. There are many other examples of methodologies and tools that
can be used to achieve high reliability. 

Now of course informally we would like to make all programs realiable, but
there is a cost/benefit trade off. For most non-safety critical programming
(but not all), it is simply not cost effective to demand total reliability.