I program in Haskell. Haskell has a strong static type system. I'll present an answer from a subjective point of view. See this Software Engineering StackExchange answer for a more technically detailed answer.
- As a haskell programmer, I always write down the type of a function before implementing the function itself. That way, just by looking at the function itself, I can tell what it does. This habit forces me to determine the "type" of mathematical objects when I am studying usual mathematics.
- By looking at the types, I can tell the structural complexity of the function, and whether it involves actions, such as changing states of the outside world.
- The type system catches a lot of errors, and in the haskell community, there is a saying "If it typechecks, it must be correct".
- Even if I do not explicitly write down the types of my function, most of it is still automatically inferred and errors are caught.
- The type system is very rich. Not only does it support polymorphic functions, but it lets you specify functions that take polymorphic functions.
- I can define algebraic data types, which means that if I am doing some, say file handling, I could actually define values
Open and Closed. Sure, this is like an enum in C, but things like Open == 0 don't make sense in Haskell.
- A Haskell programmer who wants to denote a lookup function that searches for some string in a text file will type his string as
Maybe String, indicating that the String may not be found and will return Nothing in that case. He won't return a garbage value or -1 like C programmers.
- Algebraic Data Types support recursion, which means that implementing data structures like trees are way more elegant.
- Typeclasses let me distinguish between ad-hoc and parametric polymorphism.
Finally, this is not something about Haskell in particular, but as a mathematics student interested in logic, I enjoy the connection between proofs as programs and types as propositions. This is the basis for proof assistants such as Coq.