Gradual typing is a good compromise but it introduces inconsistency and the fear of not knowing what’s under the hood, for instance your code might be typed but a library that you are using is not, or you might to forget to type one piece of your code somewhere deep inside and it would be hard to find out, that leads to uncertainty.
Thats when its wonderful, that you can simply add a simple macro at the main function, and all the inferred types are type checked.
When you are coding with certainty (are the types sound, does a function mutate the data or not, are there side effects or the function is clean, are any exceptions possible, error handling of execution, can it be null, do I have to perform bound checks) it frees your mind to worry about more important things - your actual algorithms.
Sure, coding with certainty is awesome. And not having the types stand against me at every step of the way, is one part that I like to be certain about. So I can focus on the actual algorithms.
I feel like a core part of why dynamic languages become too cumbersome to deal with in larger codebases, is because they are simply not well architected, documented, and maintained.
All things considered, I prefer spec or malli for the purposes that I used types before, since they are more flexible by offering e.g checks on ranges, they can define and enforce constraints at runtime, verify not just types, but also the shape and semantics of data, and they allow you to define custom validation logic, and so on.
They offer more functionality and restrict me less.