Ignore the children. Coq is a fantastic tool! It's unfortunate people think of Coq as an academic language. I really think it's something more people should p

Ignore the children. Coq is a fantastic tool! It's unfortunate people think of Coq as an academic language. I really think it's something more people should pull out at the workspace and not confine it to college experimentation. However the academic side of it is pretty slick. First, it's amazing how a few dozen lines of Coq can help explain the ins-and-outs of Hoare logic. (https://www.cis.upenn.edu/~bcpierce/sf/current/HoareAsLogic.html https://www.cis.upenn.edu/~bcpierce/sf/current/HoareAsLogic....). If you're into some really heady stuff and into homotopic types, the HoTT/Coq community has been explosive lately. While it's a great community, they can be a little particular when it comes to pull requests. Don't take it personally, Writing secure software will become a huge priority over the next few decades. There are many tools out there to create verifiable software, but I suspect there will always an opening for someone who can crank out rock solid Coq.