Well.. I think this is a big open problem in philosophy.

On one hand, you have things like Lean (calculus of inductive constructions), these are relatively simple formal logics (just in more practical notation) that let you define any conceivable type, which is akin to specification.

On the other hand, there is a rich set of modal and fuzzy logics that can help with aspects of reasoning in natural language. I think these can be defined in the former, but nobody has really made a good agreement as to how.

So the main difficulty is for any such language to gain traction, people who speak it.

Instead, we trained LLMs and they came up with something (evolved to reason). I think the future philosophical research will need to answer what exactly do LLMs bring to the table in terms of formalization of natural language.