> Even in Lean, you can build theories which compile but nonetheless state something different than what you actually intend.

This is just a Rice Theorem problem, right?