So we’re half way through the course I’m teaching right now and I’ve got the majority of my lecture notes for the next few weeks done. I’m glad for this because I was, truly, starting to get burned out on doing it. On the other hand, spending four weeks writing out most of my ideas for how to explain an entire quarterly course was kinda fun in a I-enjoy-teaching-but-oh-God-I-should-be-working-on-research kinda way. In any case, I’m taking a little bit of a break on posting so that I can get back to the whole higher-dimensional type theory thing and maybe I’ll go back to posting things related to papers I’m reading rather than just blah-blah-undergrad-theory-course or some of my own musings on productivity and dealing with mental illness.
On that front, though, I’ve managed to actually deal with illness and a few really crazy days in a row and still not completely fall behind in everything that I’ve wanted to get done. I’m keeping up with the course I’m teaching, I’ve been making some kind of progress on studying and research almost every day even if it’s just working out some proofs involving simple higher-inductive types over coffee in the morning. I’ve also been really making an effort to get good with Agda as opposed to just literate. To that end I’ve been doing lots of little things in Agda, like formalizing the notion of regular expressions matching a string and then proving some of the algebraic properties we generally know to be true about regular expressions. Even when I was having a very bad brain day I still managed to figure out some cute things and formalize a few little proofs about the theory of groups that I did almost 15 years ago when I first took an abstract algebra course. I’m starting to get more comfortable with the idea of using Agda as a kind of scratch paper for ideas and being able to “see” the structure of a proof as explicit proof terms. In the end, it feels way more comfortable to use explicit proof terms than it does to use tactics. I like tactics to a point, and my first theorem prover was Coq, but when I get stuck with tactics then I’m just stuck not understanding why something works. When I get stuck writing proofs in something like Agda, then I have an easier time seeing what the problem is and what I need to do about it. It’s less “magical” to me. It’s the same problem I have with Isabelle, really, where when things work they’re absolutely wonderful and amazing but when I get stuck I’m sitting there having trouble visualizing things because my mental model of tactic behavior ends up not matching the actual behavior.
Note that these are my personal experiences on theorem provers, with the understanding that other people might have a very different experience. I feel most comfortable when I have a very small number of basic constructs that I understand well, which is what theorem proving in something like Agda provides me. I am absolutely not trying to make a statement about what I think is better for everyone. Hell, I don’t think those are ever judgments that really make any kind of sense. We just find different tools that work better or worse for our individual brains.
Wow, uhh, I didn’t really expect that to turn into rambling about my feelings on theorem provers but there you go. I guess the real take away is that I’m going to try and get familiar with the Agda version of the HoTT library just because, in the end, I think I’ll find that it makes a lot more sense to me. I can relearn Coq if I truly need to, but maybe I’ll hold off on that for now and just take the more efficient path.
In any case, I should go back to reading this paper now that I actually have some time. I keep getting derailed by weird little thoughts about topology.