"The World's Most Maintainable Programming Language"

[Thomas Nelson]

I thought the paragraph about provability was interesting.  Presumably
the author refers to proofs in the spirit of "A Discipline of
Programming" from Djikstra, 1976.  Unfortunately, I don't think anyone
has writting much about this since the 70s.  I'd be interested to learn
if anyone's tried to write "weakest precondition" style specifications
for python (builtin functions, for, lambda, etc).  Or perhaps there's
some easier to understand medium?

It's worth noting that the author makes proving correctness sound like
a trivial task, which of course it's not. Consider

def collatz(n,i=0):
    if n==1:
        return i
    elif (n%2)==0:
        return collatz(n/2,i+1)
    else:
        return collatz((3*n+1)/2,i+1)

It is currently unknown whether this even terminates in all cases.