> Btw, the correctness of a program (on a turing-complete language) cannot be > statically proven. Ask Turing about it.
For the most safety critical of programmes, for which static proof is required, restrictions are placed on the use of the language that effectively mean that it is not Turing-complete. Specifically, all loops that are required to terminate require a loop variant to be defined. Typically the loop variant is a finite non-negative integer that provably decreases on every pass of the loop, which makes halting decidable. -- Tim Rowe -- http://mail.python.org/mailman/listinfo/python-list
