I'm surprised how many people are pointing to the halting problem. It might be the most well known thing about Turing Machines, but doesn't seem like the most r

I'm surprised how many people are pointing to the halting problem. It might be the most well known thing about Turing Machines, but doesn't seem like the most relevant here. Turing equivalence seems more interesting. Intuitively I'd think that type systems are supposed to be more constrained than programs they are being applied to. The fact that they are equivalent makes me think that those type systems are flawed (though I can't explain why).