Admirable to try to rebuild, but rebuilding needs to come after repairing, otherwise what is built will quickly collapse
Unless---big unless---this is what the AI Ethics team asked for as a form of repair. Just somehow I doubt it, though please correct me if I'm wrong
I think repairing things directly for Timnit is probably not possible at this point, and I'm not sure how Meg feels about that. But there's still all of the people who haven't left yet who are still on the team and probably not feeling great about it
So I hope they've spoken to the team and asked what they want, or at least plan to do that. I honestly think a public "hey, we were wrong, that was kind of messed up, sorry about that; we're going to talk to the team and ask what they want" coupled with action would help rebuild
• • •
Missing some Tweet in this thread? You can try to
force a refresh
I know grad school is always hard, but I really had three consecutive hard years: first a cruel situation at the intersection of work and my personal life that pushed me out of the state twice and almost caused me to drop out, and made me so depressed I had trouble surviving
Then just as my depression was getting better, a literal pandemic that led to my whole social support system and all of my coping mechanisms collapsing overnight, so a major relapse I also had trouble surviving at first, really
During the pandemic job search: an insurrection attempt, people I love testing positive for COVID, a serial harasser trying to use my mental illness to discredit my jobworthiness
Hi friends, I'm really excited to announce that I will start as an Assistant Professor at @IllinoisCS in October! I will be joining the already wonderful and huge @plfmse group 😊. Please apply to work with me if you're interested in building a world of proof engineering for all!
I want to acknowledge quickly that I was extremely lucky to have a difficult decision to make. I've really, really loved meeting with so many wonderful people and talking to all of you throughout the job search season, and I really do hope to stay in touch!
But I am also extremely excited about this opportunity! I'm also really excited to build connections to other midwest schools. @certifiablyrand and I have been talking about social and research connections between UIUC and UChicago!
OK here's a subproblem: Fix the logic as the calculus of inductive constructions. Is the problem of determining whether a function is extensionally equal to the identity function at a given (but arbitrary) type undecidable?
So fix arbitrary X, and an arbitrary function:
f : X -> X
You want to write a program that determines whether:
forall (x : X), f x = x
Is that undecidable?
Note that in this logic, f must always terminate! But there may be infinitely many possible x : X