4 ms·
> 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 l
by codygman 10y ago
> 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.
What if it took 3 times as long to write? I'm somewhat wildly guessing that would be unacceptable because from your perspective you don't see the benefits for it taking 3 times longer?
- burntsushi 10y agoWell, I understand the benefits, you get fewer bugs and presumably maintenance would be easier. I guess what I'm interested in is other trade offs. How close to the machine can I get with these languages? A fast regex engine these days requires SIMD, which means wherever you are needs to support using special CPU instructions. You also need to very carefully control allocations, and in my case as well, the memory layout itself. I'm interested in all the possible trade offs here, not just the type safety trade off. (That's why Rust is so appealing to me, because it nails a lot of my requirements while also giving a fairly high degree of safety.)