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

Scott David Daniels Scott.Daniels at Acm.Org
Thu Jan 22 21:32:00 CET 2009


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



More information about the Python-list mailing list