Problems harder than NP-Complete 3 years ago
It's not that humans don't write such large programs, it's that the kind of pattern that causes the exponential behavior doesn't naturally occur in long chains in any kind of written code. You can provide the pathological inputs yourself and quickly freeze e.g. OCaml's typechecker, they just don't ever naturally occur to the point of becoming a problem.
Here's an example of the pathological pattern in OCaml: https://cs.stackexchange.com/questions/6617/concise-example-...