Yes and no. You've provided an excellent introduction to the problem space, but I think natural language has a larger role in formalisms than you might expect.
The most familiar formal language grammars to most people here are programming languages. The difference between them and natural language has been categorized as the difference between "context-free grammar" and "context-dependent grammar".
The most popular context-free language is mathematics. The language of math provides an excellent grammar for expressing logical relationships. You can take an equation, write it in math, and transform it into a different equivalent representation. But why? Arithmetic. The Pythagorean Theorem would be wholly inconsequential if we didn't have an interest in calculating triangles. The application of math exists outside the grammar itself. This is why you, and everyone else here, grew up with story problems in math class.
Similarly, programming languages provide excellent utility for describing explicit computational behavior. What they are missing is the reason why that behavior should exist at all. Programs are surrounded by moats of incompatible context: it takes explicit design to coordinate them together.
If we can be explicit about the context in which a formalism exists, we could eliminate the need for ambiguity. With that work done, the incompatibility between software could be factored out. We could be precise about what we mean, and clear about what we infer. We could factor out all semantic arguments, and all logically fallacious positions. We could make empathy itself into software. That is the dream of Natural Language Processing.
I think that dream is achievable, but certainly not through implicit text models (LLMs). We need an explicit symbolic approach like parsing. If you're interested, I have been chewing on an idea that might work.