> the human's intention needs to be formally specified

Yes, that has always been the case with formal proofs. Even a mathematical proof with Lean is useless if the proven formal statement doesn’t match what the mathematician meant. And that’s why humans working with formal languages won’t be going away. Natural language is imprecise by nature, even when we have precise ideas in mind. In that case, it’s often better to specify what we mean in a formal language than in natural language.