It’s been a hell of a week, that’s for sure. I gave my first two lectures to my intro theory course without passing out, for one thing, even if I may have wanted to. The first lecture got off to a great start, in my opinion, when it turned out that someone had thought it was funny to leave permanent scented markers in the classroom in place of the dry erased markers that should have been there. It was, shall we say, annoying although I did eventually learn a cute trick for erasing said markers off the board: namely, that one should write over the offending text with an actual dry erase marker then erase. Of course, I’m still not entirely clear why we’re not just using chalkboards like civilized people.
I’ve been keeping up with my blog post goals and my word count goals by a good bit still. I’ve written over 6000 words in the past week, which as strange as it is to say, I’m kinda proud of. Most of that has been lecture notes, but there’s an essay for another site that I’m polishing up and I’ve got a series of technical posts on dependent pattern matching where, much like the simplicial sets series, y’all will get to watch me struggle with material in real time. (It’ll be the new youtube sensation: Clarissa reacts to formatting of conference papers. There’ll be swearing and drinking, assuredly.)
I’ve been keeping up on some of my github projects, but not all the ones I want to be working on. I have, though, managed to get some research done as I’m playing around with some internal-to-Agda modeling of simple higher-dimensional type theories. Umm, I have no idea how it’s going to work out so I’m terrified of letting people see it at the moment. On the other hand, by the end of the weekend maybe I’ll have something more useful to share. Oh, also, I managed to submit a couple of OS Bridge talk proposals. We’ll see if either of them gets accepted since they’re definitely a little more fringe for what’s mostly an industry conference.
Given mental disabilities and difficulty pacing myself, I think I’m actually doing really well right now all things considered. For my own health, I ended up having to essentially taken today off and spend the day disconnected from the internet so I could deal with my stress levels. The important thing, for me, is to not let myself get down to 0 sanity points (SP) since my ability to recover SP is proportional to how much I have left. My partner “made” me get off the computer, take long walks around town, and read fiction.
As far as the next week goes, I need to do a few things:
- Get back to understanding the codebase for HoTT, both Coq and Agda. I had started doing this before that cold/flu/viral-nightmare hit me a couple of weeks ago, but I need to get back to it since getting more involved in that topic is going to help my overall research.
- Work more on my Agda model
- Finish up my lecture notes through the CFG/PDA equivalence and the CFL pumping lemma
- “Grade” HW 1 which, since this homework was a self-diagnostic, just means get a feel for how all the students are doing
- Write a couple of blog posts about dependently typed pattern matching