🚀 go-pugleaf

On 10 Oct 1995, Robert Dewar wrote:

> If you are writing a safety critical program where a failure of a check
> indicates a total system failure and is a calamity, then clearly you
> have to prove that your system generates no exceptions. Once such a
> proof is complete, checks not only can be removed, but generally must
> be removed, because otherwise they complicate coverage verfication,
> where the check handling becomes deactivated code, for which special
> procedures are often necessary (and some environments simply do not
> premit deactivated code).

Perhaps then "external" checking code would be a solution. (Well, not 
completely external...) Using such "external" checking (from another 
program, library, whatever) would reduce the interdependency between the 
real code and the checking code and would also make it easier to remove 
the checking code.

> Now of course in some environments, exception handlers are added anyway
> as a defence against hardware errors, but there are other more complete
> and reliable methods (e.g. majority voting with separate computers) for
> dealing with hardware errors, and in fact the space shuttle uses exactly
> that approach.

Majority voting on different types of computers, running different OSes, 
running applications programmed in different programming languages, 
programmed by different teams, using different approaches and different 
algorithms -- that would be pretty much ideal. (Defence again hardware 
flaws -- like Pentium divide errors, OS bugs, language/compiler flaws, 
programmer error, and faulty algorithms!!!)

> So it would no surprise me or shock me to learn that if the Space Shuttle
> software was coded in Ada, it was compiled with checks off.

It wouldn't surprise me if the three computers were running programs 
written in different languages!

- Trung