I feel like this focuses too much on the recognizer than it does on the implementation of the language itself. Sure, given a grammar you can implement a correct

I feel like this focuses too much on the recognizer than it does on the implementation of the language itself. Sure, given a grammar you can implement a correct parser that accepts only valid inputs. This doesn't really buy you anything if your implementation contains a bug though. It's like an undergrad compiler course that spends all its time on parsing and how great it is then tells you almost nothing about the actual meat: the middle- and back-ends. Is your position that formally specifying the input language is a necessary first step toward formally specifying the language (operational/denotational) semantics, and eventually having a provably correct implementation? If so, why stop short at just talking about the parser when that's typically the least complicated part of any interesting input format?