A Very Happy 2023 to 2024

Home Sweet Home

• I’m home again, and it is WARM. It should be winter, but instead, I’m currently sitting in an air-conditioned room, while I have some experiments running in the background. This year, my parents and I have been watching a steady stream of Poirot, The Vicar of Dibley, Vera and even a Canadian show called Little Mosque on the Prairie. We love British murder / detective movies.
• 2023 has been a blast, and such a journey. I’m working on about three to four projects from home at this time of year, while trying to balance hanging out with family and friends. It’s tough, but I try to chip through a little bit each day. I’ve been dreaming about being back to the place with the friendly people, the warm weather, the food that doesn’t give me indigestion. The place I can get affordable health care and feel at ease with whatever they decide to do with my hair. The place that is affordable because I don’t have to constantly buy groceries from that one overpriced place within walking distance from where I live, and at this time of year, trudge through snow to do it, cursing the entire way. The place where younger people can still buy their own house and talk about how they’d like to renovate this area or that, while inviting you over for a holiday meal. The place where people expect that you can look like yourself and have an intelligent conversation, a debate between educated people on everything from law to finance to literature. The place where there is so much liquidity that people talk casually about family members who live in various countries all over the world (Wasn’t he/she last in South Africa, China, France?), or a recent trip to Dubai (earlier this year, I met someone in the airport where I travel in the town I live in the US who was from my home country, and they were in Stowe for a wedding, but planning to go to Maldives or something like that afterwards). Travelling is not a big deal; it’s like breathing air, and it’s not something people brag about; they merely mention it and bring back souvenirs for friends, and photos. My parents and myself usually walk in our neighbourhood for close to an hour early in the mornings, and we overhear conversations like “there’s this place called Banff…”, and I chuckle. It’s not perfect, but it’s nice to be back.

Some things for 2024

• Get my papers from 2023 out. It’s not even 2024 yet and this is happening. It’s kind of a shame it’s happening during my break, but then again, I’ve had committee meetings during my Christmas break, among other things, in the past. I’m incredibly proud of this stuff, even more so than my previous work. I’m super excited about these. I’ve spoken about it before, but it was important to me to be able to access and be a part of a certain standard / quality of work, and I think I’m closer to that with these upcoming works. As a mentor told me years ago about learning Haskell, “it takes what it takes”. I’m at the stage where I’d prefer something to be done properly than to churn out papers every two months. Anyways…yay 2024!
• Enjoy my first visiting position based on my area of research! I’m very excited about this, and am excited to reconnect with my peers in this area of research. The Bay is like home to me, and especially since I’m returning to the Bay for my summer internship (that I’m also super excited about, and to publish another paper, based on my area of research!), it should be fun and informative! I literally want to give my host a hug for doing so much to accommodate me!
• I want to continue learning Lean. After checking it out all the way in 2018 (after my friend, Lyle, suggested it; he’s been playing around with close to a decade at this point!), I attended a workshop on Proof Assistants for Mathematics and Computer Science (and their intersections) in February 2023 which was a nice mix of Mathematicians and Computer Scientists (really some of the best in the field in this area! It was really prestigious and I’m super grateful to have been invited and given funding!), and it gave me the courage to pick it up again, and I’ve been enjoying that. I needed to be a non-judgmental space for that to happen, and that was the space. I continued that by attending Formal Methods summer school, which kicked off an entire Spring class a year later (based on conversations I had been having with others in my lab about my experience over summer) on that that I was subsequently excluded from at my own Uni (meh), where they even used resources I had shared from the summer school I participated in (!!), never even acknowledging it was something I shared while being exclusionary, but by that time I had moved on from caring about finding that kind of support locally, much less validating any sort of need to be considered “a PL person” (I’m not because I don’t want to make languages, but I can do Formal Methods, and I understand the distinction and like Lean a lot, as it turns out).
• I also had an opportunity to attend two other Formal Methods workshops, but wasn’t able to make it this year (but am subsequently going to at least one next year!).
• In any case, our school doesn’t really have expertise in programming languages (PL) area anymore (it was literally one person, and another who subsequently left who also did some Machine Learning), so the pseudo-elitism is unwarranted..eh). It’s funny how orgs with not the strongest reputation tend to be the most pseudo-elitist (probably just insecurity I’ll guess). Some of the strongest PL people I know are pretty nice, but there is sort of a cultural problem I think that can stem from the fact that they sit somewhere along the lines of applied logic / model theory and Computer Science, so there can be this weird need to prove that “we do a lot of Maths” or something like that. Academic cultures can be strange.
• It’s a bit sad because I know some of the core proof assistant people even before grad school (at ICFP 2018 a bunch of the core Coq people were trying to lure me away from Haskell, which was hilarious, as I was a student volunteer for their workshop), and many are quite nice people (as well as a tonne of PL people); they’re good people and I wouldn’t dissuade anyone from learning Vampire or whatever if it suited their needs. I think Lean will be a great tool for Mathematicians and more normalized in the future in the Mathematics learning curriculum (and at least I’d love to push for that, too). I’m all for tools that double-check what we do, and this was one of the things I really struggled with in AI (are we speaking the same language / can we find common ground or are we just arguing about semantics?).
• I have been working 1:1 in Lean with a professor based in the UK who has been quite patient with me (we even met during the holidays, and a couple days before Christmas!), and I’m super grateful for that. What has particularly been driving me is that I’ve been learning a lot about SAT solvers, but far away from the (PO)PL-esque people (thank goodness! POPL people are cool, but I don’t enjoy people who cultivate the culty-ness of “compilers are everything are you a PL person if not please leave us you don’t like Category Theory don’t you!?” and would like to be free to explore the area for fun as it aligns with the current stuff I’m interested in). I have to admit that the Formal Methods summer school was wonderful for this; it contained some PL people, but there were also people from Model Theory and a range of other disciplines who were interested in its intersection with formal methods, and it was a really kind and friendly space. Anyways, of all the FM things, I love that SAT solvers are this tool that can be customized based on Optimization problems, Mathematics, Linguistics, Quantum, etc and they’re just super fun to learn while I’m learning Lean. Once I’m comfortable, I’d like to start formalizing some pertinent Mathematics stuff, too (not there yet; sorry!).
• Continue my Maths and Quantum journey: I did get accepted for a couple important Maths workshops, and a Quantum and Graph Theory class outside of my University, and I am really excited about those things! It’s also helped to put in perspective the fact that I rely a lot less for my dissertation work on my current University, and don’t really need to interact with them as much! Occasionally this year I’ve glanced to see what is going on, but it really doesn’t make much sense / matter to me anymore and good for them I guess (shrug).
• Of course, continue with new papers! I had to stagger the start of some people who reached out about starting projects, so I guess I’ll have to start those in the New Year. Right now I’m at capacity (until the end of Jan), but it’s nice to have built this sort of research network, and to be able to work with people I want to work with! So in short, things have been great.

Thoughts being at the intersection of Maths and Computer Science

• Computer people can make Maths people feel stupid when it comes to “computer things”. I had a conversation with a really cool functional programming group, and one person suggested that part of it is the power that comes with being “that computer guy”, and how that might affect someone’s self-esteem, so sometimes some people don’t want to let that go. Anyways, because I work at the intersection of Computing and Mathematics (these days, I spend a lot more time working with Mathematicians), I had two such situations this year where I got to see the interactions between a “Computer person” and a Mathematician. In one, a Mathematics grad student was trying to troubleshoot why their internet was not connecting and the IT person was asking them about their MAC address, and they thought because they had an Apple computer (you know, MAC could mean MacIntosh to the uninitiated and that’s a reasonable intuition tbh; they were also not a native English speaker), this had something to do with that. The IT person responded by being really condescending, and I motioned on their computer to where they could find it and they resolved the issue, and the young mathematician thanked me profusely. I was frustrated by the way the IT person had treated them. In another situation, a friend of mine who is a mathematician wanted to install Mathematics software, and the instructions just were too confusing. It made me a bit angry.
• I want to normalize that Mathematicians do code, because they do (many people in scientific (or even liberal arts) disciplines these days do some degree of coding or computational thinking. And it’s something that can be learned, especially if one has a project goal.
• I really like working with mathematicians in general, and I wish Computer people could be a bit better with respect to this regarding communication between Mathematicians and Computer Scientists. I look at some of my PL friends who are frustrated that their tool of choice wasn’t adopted as a proof assistant en masse the way say, Lean has, but I understand why now. That community must be doing something right, and as someone who started the journey in the PL community, and then felt excluded by my own peers because of elitism and insecurity (i.e. “you need to take X classes or you aren’t a real PL person” and “clearly you suck at Maths if you don’t just get this” (never mind these individuals studied the entire textbook the entire summer before taking the class!)…even though I’ve been attending POPL and went to like, 3 PL summer schools since 2017?), Lean was that community for me that got me back into really learning a proof assistant in a serious way. It’s an exciting, vibrant community, and it’s filled with some of my favourite people! I really liked that they didn’t distinguish between what type of Mathematics you came from, too! There is so much that can be learned about that!

Happy New Year

• I’m finally starting to enjoy just doing research and being left to my devices, with people who support me. I feel really great. I should have trusted my instincts to distance myself from anything that worked against my progress towards my degree, but I was able to do this successfully in Fall, and I enjoyed my Fall semester very much! I was so happy! I’m excited for 2024 and to continue my journey!
• I realized just how many people are supportive of me; I can’t tell you how many people checked in with me in Fall, from various universities. So many people want me to succeed, and I’m super grateful, even though they aren’t necessarily connected to my current institution (actually, none are). It’s important to remember that there are mentors, sponsors, and good people out there who are rooting for you! It really warmed my heart!
• Happy New Year to you!

And that’s it