From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,885dab3998d28a4 X-Google-Attributes: gid103376,public From: dewar@merv.cs.nyu.edu (Robert Dewar) Subject: Re: Ariane 5 failure Date: 1996/10/15 Message-ID: #1/1 X-Deja-AN: 189576940 references: <96100111162774@psavax.pwfl.com> <32555A39.E38@lmtas.lmco.com> organization: New York University newsgroups: comp.lang.ada Date: 1996-10-15T00:00:00+00:00 List-Id: 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.