[wyager]

I’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]

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