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).
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