Tim Rowe wrote:
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.
Having once been a more type-A, I labored for a couple of years trying
to build a restricted language that provably terminated for work on an
object-oriented database research. I finally gave it up as a bad idea,
because, in practice, we don't care if a loop will terminate or not in
database work; a transaction that takes a year to commit is equivalent
to an infinite loop for all applications that I have interacted with
(and yes, I have worked allowing four day transactions to commit).
--Scott David Daniels
scott.dani...@acm.org
--
http://mail.python.org/mailman/listinfo/python-list
