Archived tweet #9626 from the @leastfixedpoint Twitter Archive@DRMacIver Once I got into the swing of it, working with Coq was actually fun and *addictive*. I would come to, 3am, having conquered a particularly gnarly lemma, and think to myself "I'll just do one more..."