My original motivation for exploring Coq was that I was working on a compiler that repeatedly applied passes until the syntax tree stopped changing. I added som

My original motivation for exploring Coq was that I was working on a compiler that repeatedly applied passes until the syntax tree stopped changing. I added some mutable state(like a dirty bit and other things) for performance, and ended up with a few bugs that were hard to track down. One of them was that the compiler would enter an infinite loop because the syntax tree wasn't getting any less complex, but did keep changing. I didn't need any tests, because just running it demonstrated the problem. And it depended on a fairly complex interplay between many passes, so trying to individually test all the permutations would be fragile. I ended up writing a heavy-handed consistency checks that were run after every tiny update, and a tool for searching a verbose reduction log. But I made a note to later see if it was feasible to integrate termination proofs, which seemed like a useful debugging technique that I hadn't tried. I didn't want an article on compilers, because everyone already uses Haskell and Coq to write compilers, so that topic has been done-to-death already. Plus, I figured this would make it seem more approachable. In practice, you should probably just use Rails or something for your webapps.