> “Not having to” write types but having to think about them anyway is like doing math “not having to” write anything down and doing all calculations in your head. How is it an advantage to not use pen and paper to track down your train of thought as you do a complex calculation, and instead be restricted to do it only in your head?

If dynamic type systems are like not having pen and paper, then static type systems are like a teacher forcing you to "show your work" by writing every little step on pen and paper, no matter how obvious. What's interesting is finding good middle grounds.