Python from Wise Guy's Viewpoint

[Matthias Blume]

Pascal Costanza <costanza at web.de> writes:

> > There are also programs which I cannot express at all in a purely
> 
> > dynamically typed language.  (By "program" I mean not only the executable
> > code itself but also the things that I know about this code.)
> > Those are the programs which are protected against certain bad things
> > from happening without having to do dynamic tests to that effect
> > themselves.
> 
> This is a circular argument. You are already suggesting the solution
> in your problem description.

Is it?  Am I?  Is it too much to ask to know that the invariants that
my code relies on will, in fact, hold when it gets to execute?
Actually, if you think that this problem description already contains
the solution which is static typing, then we are basically on the same
page here.

> ...and BTW, please let me keep up using dynamically typed languages,
> because this works well for me!

Since I have no power over what you do, I am forced to grant you this
wish.  (Lucky you!)

> See the example of downcasts in Java.

You had to dig out the poorest example you could think of, didn't you?
Make a note of it: When I talk about the power of static typing, I am
*not* thinking of Java!

> > To make a (not so far-fetched, btw :) analogy: Consider logical
> > statements and formal proofs. Making a logical statement is easy and
> > can be very short.  It is also easy to make mistakes without noticing;
> > after all saying something that is false while still believing it to
> > be true is extremely easy.  Just by looking at the statement it is
> > also often hard to tell whether the statement is right.  In fact,
> > computers have a hard time with this task, too.  Theorem-proving is
> > hard.
> > On the other hand, writing down the statement with a formal proof is
> > impossible to get wrong without anyone noticing because checking the
> > proof for validity is trivial compared to coming up with it in the
> > first place.  So even though writing the statement with a proof seems
> > harder, once you have done it and it passes the proof checker you can
> > rest assured that you got it right.  The longer "program" will have fewer
> > "bugs" on average.
> 
> Yes, but then you have a proof that is tailored to the statement you
> have made. The claim of people who favor static type systems is that
> static type systems are _generally_ helpful.

I am not sure you "got" it: Yes, the proof is tailored to the
statement (how else could it be?!), but the axioms and rules of its
underlying proof system are not.  Just like not every program has the
same type even though the type system is fixed.

Matthias