tough-to-explain Python

[greg]

Simon Forman wrote:

> My understanding (so far) is that you (hope to) /derive/ correct code
> using formal logic, rather than writing code and then proving its
> soundness.

But to the extent you can rigorously formalise it,
all you've done is create Yet Another Programming
Language.

Which is fine, if you can come up with one that
works at a high enough level in some domain that
you can see just by looking that the program will
do what you want.

However, I suspect that you can't improve much on
what we've already got without restricting the
domain of applicability of the language. Otherwise,
you just shift the intellectual bottleneck from
writing a correct program to writing correct
specifications.

In the realm of programming language design, it's
been said that you can't eliminate complexity, all
you can do is push it around from one place to
another. I suspect something similar applies to
the difficulty of writing programs.

-- 
Greg