Yep, I agree with you - although every error should be expressible as a type error, languages like Coq where this is actually possible make writing usable code pretty difficult. I think there's a pretty wide range of middle ground, ranging from C++ to Haskell, where you get the benefit of static types without making it really difficult to write working code.