4 ms·
> If you write your code in the right way they don’t have to. That’s the point. I recommend you try working through some equality proofs in Coq, first with and
by Jweb_Guru 5y ago
> If you write your code in the right way they don’t have to. That’s the point.
I recommend you try working through some equality proofs in Coq, first with and then without coqtop / Proof General. I think you may change your mind about this rather rapidly. And many proofs get much more complex than that.
- wyager 5y agoI’ve used (and developed) plenty of proof assistants. Proofs are one very narrow domain where automation is basically a no-brainer. You don’t really lose out from the proof having high semantic arity. With normal code, you do lose out.
- Jweb_Guru 5y agoI dunno. I think the line between "normal code" and proofs is a lot blurrier than many people make it out to be, and I don't think there's a huge advantage to asking people to run a type checker or inference algorithm in their heads even if you have managed to encode all your program's invariants in the type system (which is impossible or impractical in many languages). I say that as someone who doesn't use an IDE except when I'm forced to: I know I lose out on a lot of productivity because of it, and I don't find that removing the IDE forces me to develop better or more concise code.