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
It took a long time through all of this to even want the dream I initially had again, but then with the pandemic and everything I didn't think I'd be able to do it. I feel so blessed today
• • •
Missing some Tweet in this thread? You can try to
force a refresh
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