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

[Paul Rubin]

Luis Zarrabeitia <kyrie at uh.cu> writes:
> But somehow the discussion shifted from an optional requirement (giving you 
> the chance to explicitly use 'from lock import unlock; o = unlock(obj)') 
> to "it can't be done _ever_" (using setattr/getattr is as explicit as your  
> analogous 'unlock' function).

The idea was the lock would be on the class, not on instances of the
class.  So setattr/getattr would work on instances of unlocked classes
but not locked ones.  If you wanted an unlocked instance of a locked
class, you could do it by making an unlocked subclass.

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

That's an irrelevant red herring, even if you're after provability.
It just means that there exist some correct programs that cannot be
proven correct.  What you care about is whether there is a provable
program for some particular computing task, which there almost always
is.  It doesn't matter if there are also some unprovable ones.

That is just common sense.  When you write a program you presumably
write it using some reasoning that lets you convince yourself that the
program should always work, and that's an informal proof.  (The idea of static
verification is to find the small gaps of reasoning that humans make
all the time, but once found these gaps are usually easily fixed).  

I guess one occasionally writes programs that rely on unproven and
maybe unprovable mathematical conjectures, but that is pretty rare,
especially in traditional programming where you only care about
getting correct values out.  Even in areas which do rely on unproven
conjectures (e.g. in cryptography, we rely on the conjecture that
certain functions are difficult to invert), it's usually possible to
explicitly state the conjectures that you depend on, and prove that
"if this conjecture is true then the program is correct".