[mbrock]

I'm a huge fan of static type systems and their ever helpful checkers.

For me the most difficult argument against static types is that the sweet spot remains elusive: some type systems are too simplistic (e.g. the difficulty of writing generic print in OCaml) while some are too fancy and difficult (e.g. how many people understand even most of GHC Haskell's type system?).

There's also some real problems with compiler error messages. A great type checker needs to be able to explain problems understandably, or decoding the type errors will be more difficult than tracking down a null pointer in an interactive debugger.

I wonder about the possibility of making type checkers more interactive. It can be hard to understand them because they build up lots of implicit understanding that's not apparent.