> trying to get helpful error messages Menhir is a parser generator that tries to do that: http://gallium.inria.fr/~fpottier/slides/fpottier-2015-11-oups.pdf h

> trying to get helpful error messages Menhir is a parser generator that tries to do that: http://gallium.inria.fr/~fpottier/slides/fpottier-2015-11-oups.pdf http://gallium.inria.fr/~fpottier/slides/fpottier-2015-11-ou... (Don't get scared by the first slide; the title is in French, the rest is in English.) > formally verified Menhir has been used for a formally verified parser for C: http://gallium.inria.fr/~xleroy/publi/validated-parser.pdf http://gallium.inria.fr/~xleroy/publi/validated-parser.pdf The result is in CompCert: https://github.com/AbsInt/CompCert/tree/master/cparser https://github.com/AbsInt/CompCert/tree/master/cparser