The conversation displays several misunderstandings of the role of contracts and types in programming.
Types are a syntactic form of contract. Like syntax, types are checked before the program is run.
Contracts are a semantic form of contract. They are compiled (interpreted) before/after a method is called. These concepts are complementary not exclusive.
Python, Racket, and other 'dynamically typed' languages carry around tags that some primitives check at run-time. So it is correct to call Python an 'implicitly contracted' language. Here is the problem of contracts vs types, however. If the check fails, an exception is signaled. In the good old days of Pascal, the stack trace would more or less nail down the sequence of function calls and events that produced this exception. In expressive ("higher-order") languages such as the ones discussed here, this is simply not the case. To make this claim a bit more concrete, if f calls g and stores argument h in some array and returns, and k retrieves h from the array and calls it and something goes wrong, the programmer can't easily find out that it was f that accepted h even though it was supposed to accept only methods that support readline.
The problem with Python is that it withholds this power from programmers that it grants to its implementor, namely, the power to restrict access to a method if the arguments don't work. As a result, every programmer has to create the same kind of protection code time and again.
As the success of Python demonstrates, this lack of expressive power doesn't mean a language can't succeed. It just means it makes its programmers work hard and harder -- after it lured them into its network with a pretense (its lightweight style).
Next, the lack of types isn't a problem for the development of systems. Lispers, Perlers, Schemers, Racketeers have programmed in this style for as long or longer than Pythonistas. The problem comes when the system is maintained. Time and again, the maintenance programmer has to re-discover that the third argument can be either this kind of object or that kind of object or perhaps even FALSE. Frustrated with half an hour of work, the programmer may even add a comment about what was discovered. Only to find out next time that someone else inserted another parameter into the method signature without any document.
To fix this kind of problem, an untyped programming language should come with a typed sister language, and modules in the two languages should be able to freely interoperate -- without undermining the type specs. (Technically, the type system is sound, even in the presence of untyped code.) If this pairing is available, a maintenance programmer can write down discoveries as checked type specification. The next maintenance programmer doesn't have to guess which parameter stands for what kind of argument. The annotations nail it down, and they are checked. Those parts of the system that are never touched remain untyped. The two portions of the system happily interoperate because the boundaries automatically generated type-like contracts that enforce types (even for higher-order objects) automatically.
Racket has pioneered this approach to its full extent. Some people refer to this as 'program hardening', others say 'gradual typing', we dubbed it 'from scripts to programs' -- implying that the evolution of a program should imply stabilization of some parts, and that includes typing.
Look beyond Python. It's worth it.
http://racket-lang.org/