I should probably have been more specific by writing "decide" instead of "determine", because you can absolutely 'determine' a computational property as long as you're willing to ignore false negatives. For example, it's easy enough to write a termination checker by just checking for loops and equivalent constructs (or e.g. in Idris, by requiring that all functions are total), but that will of course reject a large number of programs that do in fact terminate.
Coq is not a Turing Complete language, so Rice's theorem doesn't apply. But almost all people are not writing programs in Coq.
I think static types are great, but they don't contradict any of this.
