I've seen this attitude a couple of times before and I think it's a perfectly valid reaction to have towards these statements because you're correct. It is imp

I've seen this attitude a couple of times before and I think it's a perfectly valid reaction to have towards these statements because you're correct. It is impossible. However, type systems heavily steeped in type theory get around it being impossible by cheating. For example ... Consider the halting problem. It's pretty common knowledge that given a program and some input there's no general algorithm that tells you if that program halts when the programming language is turing complete. However, we know that every simply typed lambda calculus program halts if it passes the type checker, so did we defeat the halting problem? No we cheated because simply typed lambda calculus isn't turing complete. The problem with type theory is that sometimes it excludes good programs that we want to run just because we don't know how to prove that the program is good (or maybe it's even unprovable). So we try to develop new type theories that will allow us to prove more and more good programs are in fact good.