tough-to-explain Python

[greg]

Calroc wrote:

> It may be that flawless software is an unreachable asymptote, like the
> speed of light for matter, but I'm (recently!) convinced that it's a
> goal worthy of exploration and effort.

Seems to me that once you get beyond the toy program
stage and try to apply correctness proving to real
world programming problems, you run up against the
problem of what exactly you mean by "correct".

Once the requirements get beyond a certain level of
complexity, deciding whether the specifications
themselves are correct becomes just as difficult as
deciding whether the program meets them.

Then there's the fact that very often we don't
even know what the exact requirements are, and it's
only by trying to write and use the program that
we discover what they really are -- or at least,
get a better idea of what they are, because the
process is usually iterative, with no clear end
point.

So in theory, correctness proofs are a fine idea,
and might even be doble on a small scale, but the
real world is huge and messy!

> Just because it's unattainable doesn't make it undesirable.  And who
> knows? Maybe the horse will learn to sing.

Striving to find ways of writing less bugs is a
worthy goal, but I think of it more in terms of
adopting patterns of thought and programming that
make it more likely you will write code that does
what you had in mind, rather than a separate
"proof" process that you go through afterwards.

-- 
Greg