Article of interest: Python pros/cons for the enterprise

[Paul Rubin]

Nicola Musatti <nicola.musatti at gmail.com> writes:
> > Partial guarantees are like being a little bit pregnant.
> 
> Yes, and I'm sure your tests cover all possible paths through your code.

That is the point of type checking.  With a sound type system, "int x"
makes sure, at compile time, that x stays an integer through every
possible path through the code and never becomes a string or anything
like that.  That's why Pierce's book on type systems describes them as
"lightweight formal methods".

The happening thing in language research these days is designing more
and more powerful type systems so that you can make sure, at compile
time, that any predicate that you can describe mathematically remains
true through all possible paths through the code.  So you can have the
compiler make sure, through every possible path through the code, not
just that x is some integer, but is the actual integer that you want,
e.g. if you want x to be the largest prime number smaller than 3*y,
you can define a type for that, and then if your program to compute x
passes the type checker, it cannot compute the wrong value.

Python is a very pleasant and productive environment for banging out
code quickly that does practical things straightforwardly, but in some
ways it feels almost like assembly language, in that you have to keep
track in your head of what types of values your program is computing,
instead of being able to rely on the compiler to catch errors.