Is Python type safe?

Not in your wildest dreams.

#!/usr/bin/python

counter = 100          # An integer assignment
miles   = 1000.0       # A floating point
name    = "John"       # A string

print counter
print miles
print name

counter = "Mary had a little lamb"

print counter

When you run that you see:

python p1.py
100
1000.0
John
Mary had a little lamb

You cannot consider any language "type safe" by any stretch of the imagination when it allows you to switch a variable's content from integer to string without any significant effort.

In the real world of professional software development what we mean by "type safe" is that the compiler will catch the stupid stuff. Yes, in C/C++ you can take extraordinary measures to circumvent type safety. You can declare something like this

union BAD_UNION
{
   long number;
   char str[4];
} data;

But the programmer has to go the extra mile to do that. We didn't have to go extra inches to butcher the counter variable in python.

A programmer can do nasty things with casting in C/C++ but they have to deliberately do it; not accidentally.

The one place that will really burn you is class casting. When you declare a function/method with a base class parameter then pass in the pointer to a derived class, you don't always get the methods and variables you want because the method/function expects the base type. If you overrode any of that in your derived class you have to account for it in the method/function.

In the real world a "type safe" language helps protect a programmer from accidentally doing stupid things. It also protects the human species from fatalities.

Consider an insulin or infusion pump. Something that pumps limited amounts of life saving/prolonging chemicals into the human body at a desired rate/interval.

Now consider what happens when there is a logic path that has the pump stepper control logic trying to interpret the string "insulin" as the integer amount to administer. The outcome will not be good. Most likely it will be fatal.

Many programmers will equate static type checking to type-safety:

• "language A has static type checking and so it is type-safe"
• "language B has dynamic type checking and so it is not type-safe"

Sadly, it's not that simple.

In the Real World

For example, C and C++ are not type-safe because you can undermine the type-system via Type punning. Also, the C/C++ language specifications extensively allow undefined behaviour (UB) rather than explicitly handling errors and this has become the source of security exploits such as the stack smashing exploit and the format string attack. Such exploits shouldn't be possible in type-safe languages. Early versions of Java had a type bug with its Generics that proved it is was not completely type-safe.

Still today, for programming languages like Python, Java, C++, ... it's hard to show that these languages are completely type-safe because it requires a mathematical proof. These languages are massive and compilers/interpreters have bugs that are continually being reported and getting fixed.

[ Wikipedia ] Many languages, on the other hand, are too big for human-generated type safety proofs, as they often require checking thousands of cases. .... certain errors may occur at run-time due to bugs in the implementation, or in linked libraries written in other languages; such errors could render a given implementation type unsafe in certain circumstances.

In Academia

Type safety and type systems, while applicable to real-world programming have their roots and definitions coming from academia – and so a formal definition of what exactly is "type safety" comes with difficulty – especially when talking about real programming languages used in the real world. Academics like to mathematically (formally) define tiny programming languages called toy languages. Only for these languages is it possible to show formally that they are type-safe (and prove they the operations are logically correct).

[ Wikipedia ] Type safety is usually a requirement for any toy language proposed in academic programming language research

For example, academics struggled to prove Java is type-safe, so they created a smaller version called Featherweight Java and proved in a paper that it is type-safe. Similarly, this Ph.D. paper by Christopher Lyon Anderson took a subset of Javascript, called it JS0 and proved it was type-safe.

It's practically assumed proper languages like python, java, c++ are not completely type-safe because they are so large. It's so easy for a tiny bug to slip through the cracks that would undermine the type system.

Summary

• No python is probably not completely type-safe – nobody has proved it, it's too hard to prove. You're more likely to find a tiny bug in the language that would demonstrate that it is not type-safe.
• In fact, most programming languages are probably not completely type-safe - all for the same reasons (only toy academic ones have been proven to be)
• You really shouldn't believe static-typed languages are necessarily type safe. They are usually safer than dynamically-typed languages, but to say that they are completely type-safe with certainty is wrong as there's no proof for this.

References: http://www.pl-enthusiast.net/2014/08/05/type-safety/ and https://en.wikipedia.org/wiki/Type_system