BUburntsushi·Apr 3, 2017
> If the search is guaranteed-linear-time in any case then why the requirement for a Turing-complete language?
Because suggestions of using Turing-incomplete languages seem somewhat uninteresting to me. To be honest, I have never used one in anger, but if you told me to go write a production grade regex engine in Agda and Coq, I'd say you're nuts. It sounds like a fine experiment to do given infinite time, but I want people to actually use what I build. And I have a very strong suspicion that using one of those languages would take me 10 times as long to write it, if it's even possible at all.
I try hard to blend the practical with the theory. I'm not aware of any Turing-incomplete language that comes close enough to the practical side of things. I hope that changes as PL research advances. :-)
For the most part, my problem with your init
Read the rest
ial comment on the matter is that it neglects everything except for the "type system could have stopped it" part. But in reality, there are a host of trade offs at play given the actual choices available to me. (Even if those trade offs may be fundamentally orthogonal to the notion of type safety, they still exist and they are still things I must confront.)
I feel like an Agda/Coq implementation would be dead in the water pretty quickly. How easy or hard is it to manipulate raw byte buffers in those languages? Or memory layout? That's why Rust is such a nice tool for a regex engine, because it gives you access to the hardware at the level of C without any fuss at all, while still remaining reasonably safe.
A long time ago, we had a discussion about ASTs and property based testing. I noted that my "AST" couldn't be round-tripped with the concrete syntax accurately, and you noted that it was therefore not an AST. I'm in the middle of making that happen, and I've tried a bit harder this time around to use the type system to avoid invalid states. I do still have one that I haven't been able to rule out though, which is related to an invariant on a sequence of operations applied to a stack: https://github.com/BurntSushi/regex/blob/syntax-rewrite/rege...