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

[Mark Wooding]

Luis Zarrabeitia <kyrie at uh.cu> writes:

> Btw, the correctness of a program (on a turing-complete language)
> cannot be statically proven. Ask Turing about it.

Be careful!  Given a putative correctness-checking algorithm, there
exist programs for which the algorithm gives the wrong answer.  That
doesn't necessarily mean that there isn't a useful subset of `all
programs' which can be proven correct, or even that this subset doesn't
include all `interesting' programs.  Even so, actually constructing
algorithms which prove interesting things about all interesting programs
seems difficult.

Some people (let's call them `type A programmers') have decided that
they want to be assisted with writing correct programs -- to the extent
that they've chosen some correctness properties, and use a tool which
reject programs that it can't prove have those properties.  Since the
tool can't work for all programs, it errs on the side of caution,
sometimes rejecting correct programs.  (The properties tend to be called
`type correctness' and the tool is built into the compiler, but that's
not actually very important.)

Other people (`type B programmers') don't like having their (apparently?
possibly?) correct programs rejected.  Instead, they'd rather risk
writing incorrect programs (maybe they try to minimize the risk by
thinking very hard, or by building thorough test suites) because they
find that some of the kinds of programs the tools reject are actually
interesting and useful -- or at least fun.

I think trying to persuade a type A programmer that he wants to work
like a type B programmer, or /vice versa/, is difficult, bordering on
futile.  Type A stereotypes type B as a bunch of ill-disciplined
reckless hackers; type B stereotypes type A as killjoy disciplinarians.
Meeting in the middle is difficult.  (`We just want to add a little
safety.'  `You want to take away our freedom!'  Etc., /ad nauseam/.)

On a personal note, I've written programs in lots (/lots/) of different
languages: C, Pascal, Haskell, Standard ML, Python, Perl, Lisp, Scheme,
and assembler for various processors.  I always found programming in
permissive languages more enjoyable.  I still love ARM assembler (though
I thought the 32-bit address space changes spoilt some of its beauty),
but I don't get to write much these days; Common Lisp is now my language
of choice, but Python comes very close.  I find C too fiddly and
annoying nowadays, and its type system does an impressive job of
simultaneously being uncomfortably constraining while being too weak to
provide a satisfactory feeling of confidence in compensation.  Kernighan
summed up Pascal perfectly when he said `There is no escape.'  Haskell
is interesting: it can provide a surprising degree of freedom, but it
makes you work /very/ hard wrangling its type system in order to get
there; and again, I found I had most fun when I was doing extremely evil
unsafePerformIO hacking...

So, my personal plea.  Writing Python is /fun/.  Please let it stay that
way.

-- [mdw]