> suggests a way forward will come from formalising natural language arguments
If by this you mean "reliably convert expressions made in human natural language to unambiguous, formally parseable expressions that a machine can evaluate the same way every time"... isn't that essentially an unreachable holy grail? I mean, everyone from Plato to Russell and Wittgenstein struggled with the meaning of human statements. And the best solution we have today is to ask the human to restrict the set of statement primitives and combinations that they can use to a small subset of words like "const", "let foo = bar", and so on.
Whether the Holy Grail is unreachable or not is the question. Of course, the problem in full generality is hard, but that doesn't mean it can't be approached in various partial ways, either by restricting the inputs as you suggest or by coming up with some kind of evaluation procedures that are less strict than formal verifiability. I don't have any detailed proposals tbh
If by this you mean "reliably convert expressions made in human natural language to unambiguous, formally parseable expressions that a machine can evaluate the same way every time"... isn't that essentially an unreachable holy grail? I mean, everyone from Plato to Russell and Wittgenstein struggled with the meaning of human statements. And the best solution we have today is to ask the human to restrict the set of statement primitives and combinations that they can use to a small subset of words like "const", "let foo = bar", and so on.