Ricardo Aráoz wrote: > Actually my point was that if a program is to be trusted in a critical > situation (critical as in catastrophe if it goes wrong) then the OS, the > compiler/interpreter etc should abide by the same rules. That is > obviously not possible, so there's not much case in making the time > investment necessary for correctness proof of a little program (or > usually a little function inside a program) when the possibilities for > failure are all around it and even in the code that will run that > function. And we should resort to other more sensible answers to the > safety problem.
I don't quite see it that way. I would agree that if your OS and compiler are unreliable, then it doesn't make much sense to bend over backwards worrying about the reliability of your application. But for real safety-critical applications, you have no excuse for not using a highly reliable OS and compiler. For really critical stuff, I think the real-time OSs are usually stripped down to the bare basics. And if you are using something like SPARK Ada, the language itself is stripped of many of the fancier features in Ada itself. (There's also something called the Ada Ravenscar profile, which I believe is geared for safety-critical use but is not quite as restrictive as SPARK.) Keep in mind that the OS and compiler are typically also used for many other applications, so they tend to get tested fairly thoroughly. And remember also that you won't have extraneous applications running -- like a web browser or a video game, so the OS will probably not be heavily stressed. The most likely source of failure is likely to be your application, so bending over backwards to get it right makes sense. Then again, if you are running C on Windows, you might as well just give up on reliability from the start. You don't have a prayer. -- http://mail.python.org/mailman/listinfo/python-list
