Since you mention Python the question is not purely type-theoretic. So I try to give a broader perspective on types. Types are different things to different people. I've collected at least 5 distinct (but related) notions of types:
Type systems are logical systems and set theories.
A type system associates a type with each computed value. By examining the flow of these values, a type system attempts to prove or ensure that no type errors can occur.
Type is a classification identifying one of various types of data, such as real-valued, integer or Boolean, that determines the possible values for that type; the operations that can be done on values of that type; the meaning of the data; and the way values of that type can be stored
Abstract data types allow for data abstraction in high level languages. ADTs are often implemented as modules: the module's interface declares procedures that correspond to the ADT operations. This information hiding strategy allows the implementation of the module to be changed without disturbing the client programs.
Programming language implementations use types of values to choose the storage the values need and algorithms for operations on the values.
The quotes are from Wikipedia, but I can provide better references should a need arise.
Types-1 arose from Russel's work, but today they are not merely protect from paradoxes: the typed language of homotopy type theory is a new way to encode mathematics in a formal, machine-understandable language, and a new way for humans to understand foundations of mathematics. (The "old" way is encoding using an axiomatic set theory).
Types 2-5 arose in programming from several different needs: to avoid bugs, to classify data software designers and programmers work with, to design large systems and to implement programming languages efficiently respectively.
Type systems in C/C++, Ada, Java, Python did not arose out of Russel's work or a desire to avoid bugs. They arose out of needs to describe different kinds of data out there (e.g. "last name is a character string and not a number"), modularize software design and to choose low-level representations for data optimally. These languages have no types-1 or types-2. Java ensures relative safety from bugs not by means of proving program correctness using type system, but by a careful design of language (no pointer arithmetic) and runtime system (virtual machine, bytecode verification). Type system in Java is neither a logical system nor a set theory.
However, type system in Agda programming language is a modern variant of Russel's type system (based on later work or Per Martin-Lof and other mathematicians). The type system in Agda is designed to express mathematical properties of program and proofs of those properties, it is a logical system and a set theory.
There are no black-white distinction here: many languages fit in between. For example, type system of Haskell language has roots in Russel's work, can be viewed as a simplifed Agda's system, but from mathematical standpoint, it's inconsistent (self-contradictory) if viewed as a logical system or a set theory.
However, as a theoretical vehicle to protect Haskell programs from bugs, it works pretty well. You even can use types to encode certain properties and their proofs, but not all properties can be encoded, and the programmer can still violate the proved properties if he uses discouraged dirty hacks.
Type system of Scala is even further from Russel's work and Agda's perfect proof language, but still has roots in Russel's work.
As for proving properties of industrial languages whose type systems were not designed for that, there are many approaches and systems.
For interesting but different approaches, see Coq and Microsoft Boogie research project. Coq relies on type theory to generate imperative programs from Coq programs. Boogie relies on annotation of imperative programs with properties and proving those properties with Z3 theorem prover using a completely different approach than Coq.