(If you should first understand your problem before you write some code or if you should use code to help you understand the problem and then write more code is up to debate, of course. Typing is an invaluable tool of thought to help you understand your problem, yes, but it is just one more tool in the toolbox.)
The sad thing I noticed though is that, having hacked a mostly untyped Python code base during the last few days, making sure that all typing annotations you add to the code base are sound is a big PITA, to put it bluntly, and I would pretty much prefer to work with a statically typed language in this particular case. If your typing discipline is uncoupled from the ability to run code, people simply remove that obstacle from their way. It starts to be treated pretty much like tests and documentation: indispensable in theory, relegated to second plan in practice.
So my impression is that gradual typing almost got it right, but it may do a great disservice to overall code quality as well. I am now inclined to think that some kind of barbell strategy on typing will render better results: use both a completely untyped dynamic language such as Tcl, where everything is a string, and a static, strongly typed programming language (ideally a proof assistant with dependent types). You prototype with the former and move into production after translating your solution to the latter. If you ever need to push untyped code into production, it will be obvious to everyone involved and, since it is so decoupled, it cannot affect the quality of the statically typed codebase by any chance.