3 ms·

Can someone explain why I would ever want to use Coq? Is it mainly for algorithm researchers?

• agentultra 7y ago
  If you're a practicing programmer you may want to use a theorem prover like Coq or Lean for a couple of reasons: 1. You want to verify your algorithms, data structures, and properties are correct with regards to their specifications. For example: an OS micro-kernel, verified compiler, etc. 2. You want to derive some code with verified properties or deeply embed specifications. A lock-free and fair scheduler, an algorithm for sharing data that guarantees it doesn't leak private information, a real-time control system, etc. For an example of such a library see [0]. If you're a computer scientist you're probably more concerned with the first and proving more of your own theorems. If you're a mathematician you're (probably) more interested in new theorems (I'm not a pure mathematician, I can only speculate from what I've heard Buzzard and other mathematicians say). [0] https://hackage.haskell.org/package/containers-verified https://hackage.haskell.org/package/containers-verified