[adamnemecek]

If nothing else, it kind of follows from Curry-Howard correspondence.

What makes it okay? This Python program will not throw an exception when ran

  def f(x):
    return x

  if False:
    f(1,2)

even though the types are wrong. Are you 100% certain that you will never make a bug like this even when there are 10^13 conditions and the call stack is deeper than the Mariana trench? Note that that this is not the only type of bugs that static typing prevents.