While i subscribe to the "principle of least power"; Rice's theorem extends to even total functions in finite time. So while you can make choices on what to over/under constrain, you are still stuck with “execute it and see what the result is” in the general case.

The vast majority of code isn't the general case. Very few practical applications legitimately intend to execute halt-undecidable code for instance.

But if the language itself strongly obfuscates (or makes it difficult or impossible to express/guarantee) reliable relationships, you miss out on all the desired, and leveragable, certainty that you still intend.