> In Haskell, for example, everything happens lazily, data is
> immutable, there is a complex type system.

Also, if you've already proved the program shouldn't crash due
to type errors, you don't need to check any types as you run.