It’s probably not obvious that the parsers described above are correct. It’s also probably not obvious how you would construct a parser for our original, infix, language. People realised early on that generating parsers is both a specialised skill and one which can be automated. There are programs, called parser generators, which take a description of a formal language and generate a parser for it. For them to be able to do this the description needs to be in a suitable format. In other words one needs a formal language for the description of formal languages. If you’ve written such a parser generator you can even apply it to its own language to generate another parser generator!
Writing a parser generator is generally harder than writing a parser, and proving a parser generator always generates correct parsers is generally harder than proving that any individual parser is correct, but the great advantage is that in principle you only need to do the work once.