Does Python really follow its philosophy of "Readability counts"?

[Scott David Daniels]

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.Daniels at Acm.Org