[ojnabieoot]

It means that the type system is flexible enough to encode specific domain logic in a way that can be verified by the compiler (and therefore always be correct at runtime unless there is a bug in the compiler). Likewise, it means that plainly incorrect domain logic (eg due to a typo) is far less likely to occur than in a Python program. Some of this can be encoded by statically typed languages like C (“the average of an array of floats is a float”) but not all of it (“given a function that maps floats to floats, applying that function to an array of floats returns an array of floats”).

Python of course has none of this (“this average function actually returns the string ‘fix me!’ on some inputs because the programmer forgot to fill in and else branch”). Mypy is a useful tool but it doesn’t stop type-incorrect code from being executed and isn’t as powerful as Haskell. Likewise, the Haskell compiler certainly doesn’t catch everything, but it does completely eliminate many common Python bugs.

There is obviously a “spectrum” since no general purpose language has a truly rigorous type system.

[valenterry]

Idris is not rigorous enough?