An interview with Joey Hess

"Strongly typed" isn't enough, you also need an expressive type system, like in Haskell. Of course, you also need to make use of it properly. It's possible to write dynamically-typed (or unityped) code in almost any language.

It's not so much that the code doesn't need testing, as that the type system renders many common errors impossible, and thus does quite a bit of the testing for you in the form of static proofs at compile time. There are usually other properties not captured in the types which still need to be proved through traditional runtime tests.

In a dynamically-typed language, for example, you ought to have tests to show that a function which expects an integer responds correctly when passed a string, or some other non-integer type. In C you wouldn't write such a test, because the compiler won't let the user pass anything but an integer. Haskell is similar, except that its type system can encode much more interesting properties, so if you use it properly there are many more things that the compiler can prove about the code. As a semi-advanced example, say you have this GADT representing a simple language for managing the state of some variable:

data StateA s r where {
SetState :: a -> StateA a ();
GetState :: StateA a a;
}

The first type parameter represents the type of the state, and the second the type of the result from the action. The SetState constructor captures a value of the same type as the state, and the result type of GetState must match the state type. If you also have a function of type `runStateA :: StateA s r -> s -> (r, s)`, the compiler will take care of proving that if `runStateA (SetState 3) (5 :: Int)` terminates, it produces a value of type `((), Int)`, where the first element must be `()` and the second value can only be 3 or 5—as those are the only values of type `s` that runStateA has access to. The expression `runStateA GetState "Hello"` can only evaluate to `("Hello", "Hello")`; aside from non-termination, the runtime behavior is fully constrained by the types. The compiler will also prove that there are no side-effects or dependencies on anything other than the parameters to the function.

This does not eliminate all testing; you still need to show that `runStateA (SetState y) x == ((), y)`, since the types allow for SetState to be implemented as a no-op. It is also necessary to show that the function terminates, since the types won't prevent unbounded recursion or runtime exceptions. However, there is very little else that can actually go wrong in the implementation of runStateA.