So what happens when the Ada program runs into a failed compiler check? Does it:
* Raise an exception? If so, it's up to the programmer to treat it correctly. There are various ways to detect overflows outside Ada; it's still up to the programmer to treat them correctly. Runtime detection of the overflow (in a hopelessly untested firmware of the Therac-25!) would have brought the matter no closer to resolution.
* Abort execution? If so, is the behaviour of the program defined if execution is aborted? Because undefined behaviour from a control system is quite worse.
Normally, raise an Exception; the outermost levels of the program should probably put the machine in a "safe" state if an exception is raised during operation e.g. turn off the radiation beam etc. I would have thought this is infinitely preferable to silently continuing after an error...
SPARK Ada allows the use of source-code annotations to denote information flow in a program, and can vastly reduce the chances of these sorts of problems (at the expense of more programmer time).
Standard Ada compilers can do a reasonable job of detecting some problems at compile-time, but SPARK seems to be the favoured method for safety-critical stuff.
> I would have thought this is infinitely preferable to silently continuing after an error...
It definitely is! However, it still assumes that the exception is safely handled. The flaw in Therac 25's development process was that testing did not reveal this bug. Consequently, the error recovery process could have itself been incorrect and remain uncaught. It's tempting to think that, if error recovery is similar each time, testing it once is enough, but error recovery is as susceptible to being impeded by race conditions as any other part of the code. No uncertainty is removed this way.
It's also worth noting that a value of 0 (to which the counter overflowed) was actually a legitimate value in the Therac-25 program.
* Raise an exception? If so, it's up to the programmer to treat it correctly. There are various ways to detect overflows outside Ada; it's still up to the programmer to treat them correctly. Runtime detection of the overflow (in a hopelessly untested firmware of the Therac-25!) would have brought the matter no closer to resolution.
* Abort execution? If so, is the behaviour of the program defined if execution is aborted? Because undefined behaviour from a control system is quite worse.