3 ms·

It's fun, and it gives you new perspectives about how you might reason about program correctness in other languages as well, even if only informally in your hea

• seanwilson 7y ago
  Agree with that - I found it makes you write simpler code because you start thinking e.g. "hmm, if I write the algorithm this way, it would take forever to prove correct in Coq so it must be an overly complex approach". If you find it hard to justify robustly in your head why some code should work it's probably very difficult to prove formally which usually means there's a large surface area for bugs too. I found a big aspect of proving program correctness was formulating programs in a way first that made them easier to prove. It makes you cringe at mutable state and loops with nontrivial conditions.
• philzook 7y ago
  It is fun and useful if you're interested in formal program correctness or mathematics. Maybe it's a useful bitter pill to swallow even if you're not, but the world is a wide and wonderful place, and maybe Coq isn't the best use of your time. I think it's really interesting though, so it doesn't hurt to give it a looksy.