Getting parsing done correctly and efficiently is a requirement that pops up over and over. More work in the field is always good. Interesting paper, although I haven't heard of the parsers. I usually hear about yacc, GOLD parsing system, and so on. Like to see comparisons with most common ones for probable use cases in terms of productivity, safety, and performance.
Far as next project, Leroy's people at INRIA did excellent work in verified, LR parsers [1]. I'm not sure that anyone is building on it at the moment. Implementing that in or integrating with Rust might make for one heck of a parsing system. So long as correspondence was proven, it would be the safest one in a systems language.
The parser combinators are a common approach in functional languages. Basically, instead of generating the whole parser from a grammar, you assemble a lot of small functions, in other functions. The resulting code often ressembles the grammar very closely, and all of the intermediate parsers are very easy to test.
Proving with Coq the soundness of a parser compared to its grammar is a cool approach! The biggest problem one has when writing parsers in "safe" systems like parser generators or parser combinators, is the gaps between the input language intended by the designer, the input language described by the grammar and the input language described by the code. Anything that can reduce those gaps is welcome.
I shoul try at some point to use Coq or some SMT based system to hunt ambiguity in formats. That would make an interesting research ;)
That makes sense. The combinator approach might be verified using a form of design by contract or VCG's if it's simple functions. I'll look into them when I take the deep dive into functional programming.
Far as next project, Leroy's people at INRIA did excellent work in verified, LR parsers [1]. I'm not sure that anyone is building on it at the moment. Implementing that in or integrating with Rust might make for one heck of a parsing system. So long as correspondence was proven, it would be the safest one in a systems language.
[1] http://gallium.inria.fr/~fpottier/publis/jourdan-leroy-potti...