Since LLMs are great at coding but bad at logic, maybe an approach like this can bridge the gap? So first let it translate natural language to a formal language, from there allow it to use a logic engine to make verifiable transformations (correctness-preserving), and finally translate back to natural language.

This is great reading and a great supplement to my limited education in math, comp sci, and formal logic.

> Formal languages are basically laboratory-sized versions, or models, of natural languages.

I can understand why a hundred years ago explaining what formal is (in the context of formal languages) could have been difficult. You had to say that it means something whose form can be manipulated without "understanding", or by rules that pertain to form rather than meaning. But since the late 1930s explaining what formal means has become much simpler: it means mechanical. A formal language is one that can be precisely and accurately interpreted and manipulated by a machine.

When we talk about "formal proofs" we don't mean precise proofs, official proofs, or proofs written by a mathematician. We mean proofs written in a language, and following a procedure, that can be mechanically checked (and by a fairly basic algorithm).

While it is still a little colloquial, these days we can say that formal languages are those languages that can always be correctly interpreted by a computer. I think this captures the meaning of "formal" much more than saying these are "models of natural language".