Right, but that's precisely how Turing completeness works. It's possible to write a program that can figure out whether most real world code terminates. All Tur

Right, but that's precisely how Turing completeness works. It's possible to write a program that can figure out whether most real world code terminates. All Turing completeness tells you is that no matter how clever that program gets, there will be some programs (not necessarily 'real world programs') which it won't be able to process. The fact that the Java programming language is Turing complete doesn't prevent us being able to write programs in it (indeed it means we can write interesting programs in it!). It is just a result that tells us there are some things we can't say about ALL Java programs. This is a similar result. The fact that the Java type system is turing complete doesn't stop us expressing things with it. It just tells us there are some things we can't say about ALL Java type declarations.