OK so the name is funny and that's a whole subthread already.<p>Does anyone here use coq to build stuff? What stuff, and crucially for me, why did you pick it over isabelle or lean? Or acl2, or others<p>I want to start using theroem provers in compiler construction and getting going is a bit like trying to get sane guidance on what programming language to learn first.