As a language designer, I’ve been thinking about this sort of thing lately. It’s basically a tradeoff between how much power you give a programmer to enforce properties of their programs, and how much work you ask of them to do so.
More expressive type systems let you write programs that are more internally consistent (and, by proxy, more correct), but at the cost of more work to write the appropriate types, and to read and understand such types written by others.
A lot of PL research is going into advanced static type systems, and I think that’s a good thing, but it doesn’t necessarily translate into better programmer ergonomics or productivity.
Maybe we just need new notations for expressing types (and code!)—notations that are more in line with how people naturally think about these things.
More expressive type systems let you write programs that are more internally consistent (and, by proxy, more correct), but at the cost of more work to write the appropriate types, and to read and understand such types written by others.
A lot of PL research is going into advanced static type systems, and I think that’s a good thing, but it doesn’t necessarily translate into better programmer ergonomics or productivity.
Maybe we just need new notations for expressing types (and code!)—notations that are more in line with how people naturally think about these things.