OK so the name is funny and that's a whole subthread already. Does anyone here use coq to build stuff? What stuff, and crucially for me, why did you pick it ov

OK so the name is funny and that's a whole subthread already. 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 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.