Mark Wooding wrote: > Steven D'Aprano <st...@remove-this-cybersource.com.au> writes: > > > >> No it's not. It's *practical*. There are domains where *by law* code >> needs to meet all sorts of strict standards to prove safety and >> security, and Python *simply cannot meet those standards*. >> > > Codswallop. One can prove stuff about Python programs using the same > techniques as one uses for any other language. I've done it. Other > languages have better automated tools, it's true -- but the techniques > are basically the same. > > I've seen this kind of thinking and there are a couple of things about which I've always wondered. Let's say you formally specify an application (hey! you are a zillionaire and can afford it), and that after the app is coded you formally prove that it complies with the specification. Cool! now your app is safe? NO, because your formal proof was done over source code and the compiler has not been formally specified and proven. So your app might still fail. So let's say you have the $ to do that and you get a perfect compiler. Are you safe? NO, because the code generated by the compiler makes calls to the OS which is not specified. So let's assume you are a world leader and you spend a little war's money in fully specifying and proving an OS. Are you safe? NO, because the processor and other hardware logic has NOT been specified. And on and on.
What I've seen engineers do when they need extra safety is to put in place independently developed and operated redundant systems, at least three, and the system will do whatever two of the independent systems agree on. So I guess if I really wanted to be safe with a system I'd have it made by at least three different teams (yes, also the requirements should be written by different teams) in different languages under different OS's and different independent machines. And THEN I would have some measure of safety (and this would certainly be more cost effective than the formal specification route).
-- http://mail.python.org/mailman/listinfo/python-list