Yes, but our memory is so big and our machines can have so many states that the problem is still intractable in the general case.

But still very much solvable in the specific domains of real world applications.

You know what. I think I agree with you. I would actually go as far as to posit that most common applications don't require a Turing-Complete environment to run. If you could strip away the trouble spots and limit yourself to what you really need you can get a lot back in terms of software checking and assurance.

That's awesome. Thanks for sharing. It's nice to know that people a lot smarter than me are thinking about this already :).