TAPL is nice, and also very dense. I haven't fully read it, but my current understanding is the follow: Both the Turing Machine and the lambda calculus only describes how to act on data. They don't actually describes what the data is. So you can craft an algorithm that works well, but it can be supplied with the wrong type of data and it will goes haywire. Your only recourse is to trust the user of your algorithm.
What type does is to have a set of classes of data, then have rules between those classes. You then annotate your code with those classes (combining them if it's possible) and then your type system can verify that the relations between them hold. To the type system, your program is data.
I think undecidable means more like there are classes of problems for which there is no algorithm (that runs in finite time) can give the answer to. To square N, there is an algorithm that always works. To see if the Turing machine N halts in input M, there is not such an algorithm. The halting problem is undecidable.
There is a clever way to encode Turing machines into Diophantine equations, so Diophantine equations (linear equations