tlringer

Students under abusive advisors like this should not be punished and in fact are currently not punished. The power structures are too fundamental.

The problem is that if you cross your advisor, good luck getting a job later.

If any one of his current students are reading this, feel free to reach out to me (use ringertalia@gmail.com), and I will help you find resources that may help you while prioritizing your safety. I recommend doing this from a non-university email because university emails are not truly private.

Things to consider:

1. When under an abuser, frequently you internalize their narrative.

2. Allegedly the professor threatened to kill him if he "ruined his reputation."

3. If he was an international student (I do not know if he was), he could quite literally lose his visa for losing his spot in the program.

4. If your advisor hates you and you haven't managed to safely switch advisors, good luck getting a letter for any future academic pursuits. (Unless you're willing to speak out about what happened, or you have someone willing to write an explanatory letter on your behalf.)

5. When you're being abused and threatened with retaliation for speaking out and so on, you aren't thinking rationally. It's really traumatic and scary, and sometimes it's hard to imagine a path out that is tolerable, and death sounds safer and easier.

We in academia need to respond by setting up better systems to recognize and safely escape abusive situations without permanent harm to one's career and mental or physical wellbeing. And also by making those systems known to students and very easy to access and use.

Someone really, really, really needs to get this professor's current students to safety immediately. Don't forget that shortly before the student's suicide, according to a screenshot of a conversation with the student who took his own life (same Medium account, earlier article), the professor threatened to kill the student if he "ruined his reputation." His students are not safe and the focus should be on making sure they are safe.

Finally, an excuse to nap

I'm really happy with the framing of this article, and with the nuance in discussing other ITPs and the history of ITPs!

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.

I have learned more about Kevin and feel bad for bringing up the heckling thing now. I would ignore that part of what I said.

It is my understanding that functional extensionality in Lean itself follows from the axiom propositional extensionality, so in that sense LEM is still a consequence of an axiom. The core theory of Lean is constructive.

That makes sense! I just wish discussion on this end would stay nuanced: In that case Lean has great library support for classical mathematics. This is an important distinction because it is something that the authors of other constructive proof assistants can focus on if they want to reach more mathematicians.

I like these lecture notes: https://staff.math.su.se/anders.mortberg/papers/cubicalmetho...

But if that is too hard to read, I recommend telling Anders directly when you get confused. He is open to improving the notes.

Lean is not classical. I don't know where the idea that Lean is classical is coming from. Lean is constructive. It is consistent with classical axioms, just like Coq is, and just like Cubical is in the propositional fragment. Isabelle/HOL on the other hand is classical, and is quite a natural choice if classical logic is what you want, which is why mathematicians have been using it for decades now.

I know Kevin. He does good work. He also heckled every talk at ITP, including my own, in the middle to express his opinions. I have never met another researcher in my life who does that. Media outlets interview him and not the other 50 years of researchers doing work on proof assistants and using them both for mathematics and for verifying systems. I wrote a whole book about the history of program verification and for sure nobody has ever interviewed me about it. Kevin is loud and bold, that is why his opinions spread like fire. But they are just that, opinions.

Lean isn't classical.

Lean is the calculus of inductive constructions with uniqueness of identity proofs. Classical logic in Lean requires using axioms.

It does. And if classical logic is what they like, they can use Isabelle/HOL just as nicely. It is classical. It has wonderful automation. Kevin gets attention because he is bold, not because he is correct.

Anonymous comments are cowardly; please show yourself. If you stay anonymous I am not aware of power dynamics, and I cannot adjust my response accordingly.

There is RedPRL, there is also cubical Agda. I think cubical Agda is the best developed so far. It lacks automation. But that is not fundamental, it is thanks to the philosophies of the people involved.

Lean is not weak, it just commits to something called Uniqueness of Identity Proofs (UIP). This is inconsistent with Univalence, a property that cubical type theories have. Necessarily, neither system can express "all of math." So it goes.

Leo chose UIP to get a novel way to get really powerful automation of equality proofs. Leo is very, very good at this; this is his whole shindig. But he had to hack around things a bit in order to get what he wanted. The paper by Bas and his student shows that in cubical, you don't have to hack around things; this automation of equality proofs arises in the natural way.

The gap is not fundamental, and it irritates me when it is attributed to the choice of UIP. The reason Lean is so useful is because the people working on it are good at building automation. The people working on cubical are much more interested in foundations. We need people who are interested in automating cubical; once we get that, the proof assistant that arises from it will be better than anything we have ever seen.

The idea of Lean being suitable for all of math is sensationalist and Kevin knows it. Lean being committed to UIP already rules out many kinds of mathematics. Furthermore, the kind of automation possible in Lean is also possible in univalent theorem provers with the right implementation (e-graphs). They are actually easier in cubical than in Lean (see the 2 pager by Bas Spitters and his masters student).

The difference is that no cubical proof assistant has been implemented by Leo de Moura. Get Leo de Moura to implement cubical, and you will have a proof assistant more powerful than you could ever imagine, built on extremely satisfying foundations.

If he means there was a time "before" time, wouldn't we need some metatheoretical notion of time to even state that? Like how can we state that in our system if our time begins at the big bang? I don't get it

Forgive my ignorance, but what does it mean for something to exist before the big bang? What happens to time at the boundaries?

Probably much less. It is not just running form that makes elite runners efficient. Due to both genetics and training, their bodies use fuel more efficiently, too.

Elite runners tend to burn much less than normal runners over the same distance, since they are typically lighter and more efficient.

This race didn't follow the rules so he could do whatever he wanted. Under official rules, you can have a custom drink placed on a table, which you run by and pick up yourself. Most marathons with an elite wave do this for elite runners. Nobody can hand you your drink.

However, it is not common to have very calorie-dense drinks because it is just not necessary over that distance. You want a little bit of carbohydrate so that you don't deplete your glycogen stores or get low blood sugar. That is about it. So most runners will consume maybe 200-300 calories during a marathon. Elite runners will typically consume less, again since they are more efficient.

The Nike shoes are legal, though controversial. Give it a few more years of further improvements to the shoe technology, and they will probably be banned and asterisks will be placed next to every record, like in swimming when technology got too good.

That is all of LetsRun. It is an incredibly toxic community full of experts and trolls.

For one, pacemakers have to enter the race and start the race with him. You can't have pacemakers enter partway. They all have to be eligible to hit the record too if they are capable. Per IAAF rules, pacemakers are basically just competitors that you pay to go out too fast and drop out partway.

Also just not a sanctioned course, not proper testing protocol for doping, not open to other competitors, and so on.

(Former USATF apprentice official, though stopped officiating once I started grad school)

This is a really interesting idea. In some sense, you can say a proof script is "almost correct" if it proves a slightly different theorem.

I suspect the one difficulty there would be finding such incremental changes on Github. It was surprisingly difficult to find small changes to specifications in Git history for a different project that I did. Too many large commits and too much history revision, so you often lose the incremental changes. Still, it is worth trying.

That's a neat idea. It would mostly help for gathering data from beginners, which would be very skewed, but I'm sure it could still be useful, especially for developing tools to help beginners.

As an example of using semantic information, you might define a bunch of functions that take two natural numbers and return some result. Then you might write some proofs about those functions.

Let's say you write those proofs via induction over the natural numbers. You can choose between arguments to induct over if your functions take multiple inputs. The most effective choice often depends on the definitions of your functions. This means to pick the best argument, already you need to unfold your definition. Chances are you do that unfolding in your head, not using a tactic, or at least not one that you keep in your final proof.

So already, an ML technique for ITPs that does not unfold definitions in goals for more information is missing out on the essential piece that makes a user choose one argument for induction over another, even when syntactically the hypotheses and goals may look identical (I can define "add" to break down the first argument or the second argument, my call).

In general, I think the ITP community likes to pretend that we are using tactics to interact with a black box, but in practice, most of us have internalized heuristics that involve introspecting on the structures of terms and types. So any model that lacks the information to internalize those heuristics is missing out.

There has been a lot of work like this popping up in the past year. I think it's somewhat promising, but for ML for ITPs to really become useful, I think the models need to better take into account semantic information about terms and types and not just tactics. And this is not easy, because Coq's logic is higher-order and dependently typed, and most work in ML for PL deals with much simpler logics. Still, anything that helps with the tedium is welcome.

Another problem is that you will very rarely find examples of failing proofs, since users rarely commit them. I'm working on a joint UW-UCSD project on collecting and analyzing development data, and this is one of the goals. But our dataset is not very large, since it is hard to get users to agree to something so invasive, and there are still only 1000 or so active Coq users in total in the world right now.

Another big problem is that it is very, very difficult to define what it means for a proof to be "almost" correct. This makes it difficult to apply many existing techniques fruitfully.

Nonetheless, I think the general spirit is right. The biggest gains in proof automation in ITPs this decade are going to come from automation that makes use in some way of existing proofs, rather than starting from scratch and "blindly" (often very effectively or even decideably for certain fragments of the logic or certain domains if the user knows the right tactic to call) searching for some term with a given type.

I developed a huge crush on a very close friend shortly after my ex broke up with me. He caught on and told me he wasn't interested. We are even better friends now than we were then. We just took a few weeks apart and then resumed. I appreciated the transparency, but the ambiguity was still necessary for developing the crush to begin with.

I met a few people on OKCupid during that time and was not sure if I had the potential to like them or not because my ex was in close proximity and that was messing with my feelings a lot. I told them to just be friends and expect nothing else, and that I'd revisit the question in June. One said he was out; that was fine, I'd just met him. The other is one of my close friends now, even though the answer was still no in June.

This happened with someone who was already my one of best friends, too. He was hurt for a few weeks, but then everything went back to normal and now we are still best friends.

I can understand why this would be hard after a long-term relationship with someone you are in love with. My ex and I are still very, very far from friendship, despite both wanting it eventually. But with someone you have never even been in a relationship with? It's ridiculous to take rejection personally and let it get in the way of your friendship.

My current boyfriend, I met when I was running away to another state to get away from my ex. I was looking for people to practice my Russian with. The expectation was that we would hang out and speak Russian once in a while, and then probably never see each other once I returned home. And now I'm in a very rewarding long-distance relationship.

I don't think it's that the stakes made it exciting. I think it's that the lack of expectations made it feel safer.

It is just the opposite. So you feel OK getting to know the person just to get to know them. Then your heart does its own thing. And that's why I think people say that love "just happens" and not to look for it. You can look for it, but by doing that, you are setting expectations that might preclude you from getting to know the person you might at some point love, just for the sake of knowing them. Not specifically to love them.

The ambiguity is good.

How do we gather divorce statistics? Because divorce is an extreme case of what you mention, and a very common one.

One thing that I think these posts always ignore is that, for a lot of us, the ambiguity over whether or not it is a date is an essential piece of the puzzle. So going in knowing it's a date takes away all of the magic necessary to fall for someone else. I always meet someone as soon as I give up on online dating.

If I were single again, I think I would like an app that deliberately makes it ambiguous whether someone likes you or just wants to hang out with you. You'd have to figure that out yourselves. So you'd choose people you genuinely enjoyed spending time with, which would increase your potential dating pool, but you wouldn't go into it without the magic of ambiguity.

Data is always cool though.