This book and the Coq proof assistant are what pushed me to learn Emacs. The 'coqide' application my class (CSE 505 at UW) used was not a good text editing expe

This book and the Coq proof assistant are what pushed me to learn Emacs. The 'coqide' application my class (CSE 505 at UW) used was not a good text editing experience. Emacs + Proof General by contrast were incredible. It's important to have a solid on-ramp for beginners. I tried using Emacs for a Java project in my next class, but I never managed to set up anything as nice as the IntelliJ IDE. I'm sure setting up something nicer is possible, but first impressions matter.