For the most part this cognitive load already exists in order to write correct programs. Types don’t just appear when a type checker is present. Type systems only add on the additional burden of needing to understand the formalization of that intuition. It’s not an insignificant burden, but it’s a much smaller gap than learning to intuit about programming correctly in the first place.
It depends on what you mean by "correct". If it means "it does what I need it to do and I can move on with my life", then no, the cognitive load doesn't already exist, and formalized type theory in many cases adds an incredible amount of cognitive load.
I know that in many cases "correct" means a lot more than that, such as in proper software engineering contexts when building a program/system that needs to live and evolve for a long time among many people. I write that kind of software all the time, and I always use static type systems for it.
But I also write a bunch of ad-hoc, one-time-use programs, and I'm very glad that I don't need to reason about abstract type theory in order to parse a CSV file and add up some columns to send to a colleague.
I don’t care if my throw away CSV munger is formally safe/sound or maintainable. I care if it gives me correct results, once, as quickly and effortlessly as possible. Which is why very few people fire up GHCi/rustic/javac for that, but instead use awk/shell/Python or something similar.
OTOH, sometimes the CSV munger one writes today is still in use five years later, when the input CSV has a UTF-8 character for the first time, and suddenly it crashes and no-one knows where the bug could even be.
UTF-8 support is completely orthogonal to static typing. There are dynamically typed languages that handle it great, and statically typed languages which have garbage support for it.
In general I know what you mean though. “What if this CSV parser turns out to be really important?” If you think there’s a high probability of that, do it in a statically typed language then. 99.9% of data munging I’ve done have been throwaway programs to answer a question to inform some decision or help refine a mental model.
