Importantly, this is only true if you also want to be correct when you say "unsafe." The entire field of static analysis exists and happily moves along solving

Importantly, this is only true if you also want to be correct when you say "unsafe." The entire field of static analysis exists and happily moves along solving undecidable problems in practical ways every single day. There are just some false positives or false negatives (or both) depending on how you choose to design a system. "Does this program ever encounter a typing error at runtime" is an undecidable problem. Yet we have type systems baked right into our compilers that happily reject all programs that might encounter a typing an error at runtime. They just also reject some other programs too.