It is possible to determine interesting properties of programs if you weaken your requirements to approximations and/or add significant constraints. You can maintain properties by construction if you only allow yourself to use certain kinds of building blocks in assembling programs. The less powerful your computational model, the easier it is to prove things about it.
The core idea of a type system is to form a symbolic representation of the semantics of your program which is simpler than the program itself, so that you can prove properties of that simpler system instead of the intractable problem of doing so for the actual program. (If you aren't careful, your type system could end up sufficiently powerful that it is itself undecidable, and you're back where you started.)