No, I'm not misunderstanding, and you are pushing goalposts. The majority of programs above a certain size would benefit tremendously if they were "matching a specification". Sure, the specification itself may not be fully correct, but a lot, if not most bugs, are code that would go against such a specification.
> Also, just think about this: what bugs have you had in your software historically? How many of those do you believe would've been prevented by a type system like Haskell's??
I program Haskell all the time, and I encounter "non-bugs" where the compiler prevented me from doing something, which other languages would not have, on the regular.
> (though I do use typed languages like Java and Kotlin)
Those are not even close to a Hindley-Milner based type system like the one in Haskell.
> Also, just think about this: what bugs have you had in your software historically? How many of those do you believe would've been prevented by a type system like Haskell's??
I program Haskell all the time, and I encounter "non-bugs" where the compiler prevented me from doing something, which other languages would not have, on the regular.
> (though I do use typed languages like Java and Kotlin)
Those are not even close to a Hindley-Milner based type system like the one in Haskell.