[withtypes]

Saying Lean "rules out many kinds of mathematics" and not giving a single example, sounds more sensationalist to me. I also don't see what's wrong with anonymous comments as long as they are constructive and people are nice.

I don't know Kevin as well as you do (apparently) but maybe he is just ignorant on the topics you know so much about. Why something gets attention of media (Quanta Magazine?) is complicated. From your comments, you also seem very "bold".

[tlringer]

I'm a woman though, and women rarely get positive attention for anything in CS. I'm bold because as a woman in the field you need to be bold to survive as a researcher. In the type theory and proof assistant worlds there are only a handful of us. A typical ratio at a conference for proof assistant research is 1 woman for every 40 men.

Anonymous comments scare me because there are (a few, thankfully not many) abusive people in the PL community I am afraid of engaging with. I don't want to accidentally find myself arguing with one of them. I need to know when to exit the conversation.

Proof relevant mathematics, higher category theory, lots of topology. Sorry. I don't spend all of time on HackerNews, I sometimes don't get around to responding to things. I am talking to Kevin about this framing so we can figure out how to make it healthier in the future. Some of my comments about Kevin were likewise out of line because I interpreted some of our previous interactions as rooted in a gender-based power dynamic when they were actually just rooted in something Kevin finds difficult and wants to do better at, and that is my honest mistake.