4 ms·

Just say "cock", with a straight face, not laughing and serious, and people will not laugh. People will know it's the proof assistant. Same when saying "Hoare

• colanderman 10y ago
  Although I think the hairy ball theorem [1] is an exception to this logic. [1] https://en.wikipedia.org/wiki/Hairy_ball_theorem https://en.wikipedia.org/wiki/Hairy_ball_theorem
• deleted 10y ago
  [deleted]
• steego 10y ago
  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.
  • deleted 10y ago
    [deleted]