> However, I don't want to disparage the tutorial nature too much, because learning to "think in Coq" has dramatically changed the way I reason about even traditional pencil and paper proofs, for the better.

That sounds intriguing, but I wonder if being more rigorous also means being much slower in completing proofs and if practicality is lost (?)