[still_grokking]

I agree that something like "over-typing" exists. But where it starts is imho very context dependent.

For the lowest level (e.g. an OS) you really want an extremely strict regime. Bugs are "simply not allowed"…

For application level code I think it depends. Nobody would finish anything if the requirement would be to formally verify all your code.

The other thing is: How far you can get before "over-typing" starts is also dependent on the language and how powerful it's type inference system is. Rust is quite weak in this regard.

In a language where the compiler can pass context for you one can have very strong guaranties without making working with the code too awkward. Of course, changing the code will need work. But that's the whole point of type systems: If you change something the compiler will tell you any places where something needs repair. In less strongly typed languages you can just pray that your tests are good enough to cover the changes.

In case of changes a good compiler will even rewrite the trivial cases for you if you ask, and just leave what really needs human oversight. But such automatic rewriting (with the guaranty that nothing went wrong!) works only if you had very strong types in the first place.