> Is the remaining 10% of “formal correctness” worth the extra volume of characters on the screen? Yes, if only just for the ease of large-scale refactorings.

> Is the remaining 10% of “formal correctness” worth the extra volume of characters on the screen? Yes, if only just for the ease of large-scale refactorings. And "extra volume of characters" is very limited if you use a modern language. In Haskell you could even not write a single type annotation in all of your code, although that's not recommended. I doubt most people who like static types only do so because of autocomplete.