When was this a non-religious issue? But I believe the problem is following: Either the type system is incomplete (there are programs out there that you might want to run but won't be able to), or it's unsound (some programs will get a pass the type checker but fail at run time), or the type system will be so complex as to being undecidable. Since people generally aren't happy with number one, you either have to rely on the programmer (number two) or force everything to pass through a potentially loopy process every time you compile something (number three)

Ot, one might go the Qi/Shen route...