§ Stuff I learnt in 2019


I write these retrospective blog posts every year since 2017. I tend to post a collection of papers, books, and ideas I've stumbled across that year. Unfortunately, this year, the paper list will be sparser, since I lost some data along the way to the year, and hence I don't have links to everything I read. So this is going to be a sparser list, consisting of things that I found memorable .
I also re-organised my website, letting the link die, since keeping it up was taking far too many cycles (In particular, CertBot was far too annoying to maintain, and the feedback of hugo was also very annoying). I now have a single file, the README.mdof the bollu/bollu.github.io repo, to which I add notes on things I find interesting. I've bound the i alias (for idea) on all my shells everywhere, to open the README.md file, wait for me to write to it, run a git commit so I can type out a commit, and then push. This has been massive for what I manage to write down: I feel like I've managed to write down a lot of one-liners / small facts that I've picked up which I would not otherwise. I'm attempting to similarly pare down other friction-inducing parts of my workflow. Suggestions here would be very welcome!
If there's a theme of the year (insofar as my scattered reading has a theme...), it's "lattices and geometry". Geometry in terms of differential geometry, topology, and topoi. Lattices in the sense of a bunch of abstract interpretation and semantics.

§ Course work: optimisation theory, quantum computation, statistics


My course work was less interesting to me this time, due to the fact that I had chosen to study some wild stuff earlier on, and now have to take reasonable stuff to graduate. However, there were courses that filled in a lot of gaps in my self-taught knowledge for me, and the ones I listed were the top ones in that regard.
I wound up reading Boyd on optimisation theory , Nielsen and Chuang for quantum computation, where I also solved a bunch of exercises in Q# which was very fun and rewarding. I'm beginning to feel that learning quantum computation is the right route to grokking things like entanglement and superposition, unlike the physics which is first of all much harder due to infinite dimensionality, and less accessible since we can't program it.

§ Formal research work: Compilers, Formal verification, Programming languages


My research work is on the above topics, so I try to stay abreast of what's going on in the field. What I've read over the past year on these topics is:








§ Internship at Tweag.io over the summer: Hacking on Asterius (Haskell -> WebAssembly compiler)



I really enjoyed my time at Tweag! It was fun, and Shao Cheng was a great mentor. I must admit that I was somewhat distracted, by all the new and shiny things I was learning thanks to all the cool people there :) In particular, I wound up bugging Arnaud Spiwack , Simeon Carstens , and Matthias Meschede quite a bit, about type theory, MCMC sampling, and signal processing of storm clouds.
I wound up reading a decent chunk of GHC source code, and while I can't link to specifics here, I understood a lot of the RTS much better than I did before. It was an enlightening experience, to say the least, and being paid to hack on a GHC backend was a really fun way to spend the summer.
It also led me to fun discoveries, such as how does one debug debug info?
I also really loved Paris as a city. My AirBnb host was a charming artist who suggest spots for me around the city, which I really appreciated. Getting around was disorienting for the first week or so, due to the fact that I could not (and still do not) really understand how to decide in which direction to walk inside the subways to find a particular line going in a particular direction .
The city has some great spots for quiet work, though! In particular, the Louvre Anticafe was a really nice place to hang out and grab coffee. The model is great: you pay for hours spent at the Anticafe, with coffee and snacks free. They also had a discount for students which I gratefully used. I bumped into interesting artists, programmers, and students who were open for conversation there. I highly recommend hanging out there.

§ Probabilistic programming & giving a talk at FunctionalConf


This was the first talk I'd ever given, and it was on probabilistic programming in haskell. In particular, I explained the monad-bayes approach of doing this, and why this was profitable. The slides are available here .
It was a fun experience giving a talk, and I'd like to do more of it, since I got a lot out of attempting to explain the ideas to people. I wish I had more time, and had a clearer idea of who the audience was. I got quite a bit of help from Michael Snoyman to whip the talk into shape, which I greatly appreciated.
The major ideas of probabilistic programming as I described it are from Adam Scibior's thesis:

Along the way, I and others at tweag read the other major papers in the space, including:

§ Presburger Arithmetic


Since we use a bunch of presburger arithmetic for polyhedral compilation which is a large research interest of mine, I've been trying to build a "complete" understanding of this space. So this time, I wanted to learn how to build good solvers:

§ Open questions for which I want answers


I want better references to being able to regenerate the inequalities description from a given automata which accepts the presburger set automata. This will allow one to smoothly switch between the geometric description and the algebraic description. There are some operations that only work well on the geometry (such as optimisation), and others that only work well on the algebraic description (such as state-space minimisation). I have not found any good results for this, only scattered fragments of partial results. If nothing else, I would like some kind of intuition for why this is hard .
Having tried my stab at it, the general impression that I have is that the space of automata is much larger than the things that can be encoded as presburger sets. Indeed, it was shown that automata accept numbers which are ultimately periodic.

But yes, it's known that automata accept a language that's broader than just first order logic + "arithmetic with +", which means it's hard to dis-entangle the presburger gits from the non-presburger bits of the automata.

§ Prolog


I wanted to get a better understading of how prolog works under the hood, so I began re-implementing the WAM: warren abstract machine . It's really weird, this is the only stable reference I can find to implementing high-performance prolog interpreters. I don't really understand how to chase the paper-trail in this space, I'd greatly appreciate references. My implementation is at bollu/warren-cpp. Unfortunately, I had to give up due to a really hard-to-debug bug.
It's crazy to debug this abstract machine, since the internal representation gets super convoluted and hard to track, due to the kind of optimised encoding it uses on the heap.
If anyone has a better/cleaner design for implementing good prologs, I'd love to know.
Another fun paper I found in this space thanks to Edward Kmett was the Rete matching algorithm , which allows one to declare many many pattern matches, which are then "fused" together into an optimal matcher that tries to reuse work across failed matchers.

§ General Relativity


This was on my "list of things I want to understand before I die", so I wound up taking up an Independent Study in university, which basically means that I study something on my own, and visit a professor once every couple weeks, and am graded at the end of the term. For GR, I wound up referencing a wide variety of sources, as well as a bunch of pure math diffgeo books. I've read everything referenced to various levels. I feel I did take away the core ideas of differential and Riemannian geometry. I'm much less sure I've grokked general relativity, but I can at least read the equations and I know all the terms, so that's something.

§ Discrete differential geometry


I can't recall how I ran across this: I think it was because I was trying to get a better understanding of Cohomology, which led me to Google for "computational differential geometry", that finally led me to Discrete differential geometry.
It's a really nice collection of theories that show us how to discretize differential geometry in low dimensions, leading to rich intuitions and a myriad of applications for computer graphics.

§ Synthetic differential geometry


It was Arnaud Spiwack who pointed me to this. It's a nice axiomatic system of differential geometry, where we can use physicist style proofs of "taking stuff upto order dx", and having everything work upto mathematical rigor.
The TL;DR is that we want to add a new number called dx into the reals, such that dx^2 = 0. But if such a number did exist, then clearly dx = 0. However, the punchline is that to prove that dx^2 = 0 => dx = 0 requires the use of contradiction!
So, if we banish the law of excluded middle (and therefore no longer use proof by contradiction), we are able to postulate the existence of a new element dx, which obeys dx^2 = 0. Using this, we can build up the whole theory of differential geometry in a pleasing way, without having to go through the horror that is real analysis. (I am being hyperbolic, but really, real analytic proofs are not pleasant).
I began formalizing this in Coq and got a formalism going: bollu/diffgeo.
Once I was done with that, I realised I don't know how to exhibit models of the damn thing! So, reading up on that made me realise that I need around 8 chapters worth of a grad level textbook (the aptly named Models of Smooth Infinitesimal Analysis ).
I was disheartened, so I asked on MathOverflow (also my first ever question there), where I learnt about tangent categories and differential lambda calculus. Unfortunately, I don't have the bandwidth to read another 150-page tome, so this has languished.

§ Optimisation on Manifolds


I began reading Absil: Optimisation on matrix manifolds which describes how to perform optimisation / gradient descent on arbitrary Riemannian manifolds , as well as closed forms for well-known manifolds. The exposition in this book is really good, since it picks a concrete manifold and churns out all the basic properties of it manually. The only problem I had with the books was that there were quite a few gaps (?) in the proofs -- perhaps I missed a bunch.
This led me to learn Lie theory to some degree, since that was the natural setting for many of the proofs. I finally saw why anyone gives a shit about the tangent space at the identity: because it's easier to compute! For a flavour of this, consider this question on math.se by me that asks about computing tangent spaces of O(n)O(n).

§ AIRCS workshop


I attended the AI risk for computer scientists workshop hosted by MIRI (Machine intelligence research institute) in December. Here, a bunch of people were housed at a bed & breakfast for a week, and we discussed AI risk, why it's potentially the most important thing to work on, and anything our hearts desired, really. I came away with new branches of math I wanted to read, a better appreciation of the AI risk community and a sense of what their "risk timelines" were, and some explanations about sheaves and number theory that I was sorely lacking. All in all, it was a great time, and I'd love to go back.

§ P-adic numbers


While I was on a particularly rough flight back from the USA to India when coming back from the AIRCS workshop, I began to read the textbook Introduction to p-adic numbers by Fernando Gouvea , which fascinated me, so I then wrote up the cool parts introduced in the first two chapters as a blog post . I wish to learn more about the p-adics and p-adic analysis, since they seem to be deep objects in number theory.
In particular, a question that I thought might have a somewhat trivial answer ( why do the p-adics use base p in defining norm ) turned out to have answers that were quite deep, which was something unexpected and joyful!

§ Topology of functional programs



Both of these describe a general method to transfer all topological ideas as statements about computability in a way that's far more natural (at least for me, as a computer scientist). The notion of what a continuous function "should be" (keeping inverse images of open sets open) arises naturally from this computational viewpoint, and many proofs of topology amount to finding functional programs that fit a certain type. It's a great read, and I feel gave me a much better sense of what topology is trying to do.

§ Philosophy


I've wanted to understand philosophy as a whole for a while now, at least enough to get a general sense of what happened in each century. The last year, I meandered through some philosophy of science, which led me to some really wild ideas (such as that of Paul Feyerabend's 'science as an anarchic enterprise' which I really enjoyed).
I also seem to get a lot more out of audio and video than text in general, so I've been looking for podcasts and video lectures. I've been following:


I also attempted to read a bunch of philosophers, but the only ones I could make a good dent on were the ones listed below. I struggled in writing this section, since it's much harder to sanity check my understanding of philosophy, versus mathematics, since there seems to be a range of interpretations of the same philosophical work, and the general imprecise nature of language doesn't help here at all. So please take all the descriptions below with some salt to taste.



§ Information theory


I've been on a quest to understand information theory far better than I currently do. In general, I feel like this might be a much better way to internalize probability theory, since it feels like it states probabilistic objects in terms of "couting" / "optimisation of encodings", which is a perspective I find far more natural.
Towards this aim, I wound up reading:


§ Building intuition for Sheaves, Topoi, Logic


I don't understand the trifecta of sheaves, topoi, geometry, and logic, and I'm trying to attack this knot from multiple sides at once.

All of these provide geometric viewpoints of what sheaves are, in low-dimensional examples of graphs which are easy to visualize. I'm also trudging through the tome:

which appears to follow the "correct path" of the algebraic geometers, but this requires a lot of bandwidth.

This is a hardcore algebraic geometry textbook, and is arguably great for studying sheaves because of it. Sheaves are Chapter 2, and allows one to see them be developed in their "true setting" as it were. In that Grothendeick first invented sheaves for algebraic geometry, so it's good to see them in the home they were born in. Once again, this is a book I lack bandwidth for except to breezily read it as I go to bed. I did get something out from doing this. I'm considering taking this book up as an independent study, say the first four chapters. I'll need someone who knows algebraic geometry to supervise me, though, which is hard to find in an institute geared purely for computer science. (If anyone on the internet is kind enough to volunteer some of their time to answer questions, I'll be very glad! Please email me at rot13(fvqqh.qehvq@tznvy.pbz))

§ The attic


This section contains random assortments that I don't recall how I stumbled across, but too cool to not include on the list. I usually read these in bits and pieces, or as bedtime reading right before I go to bed to skim. I find that skimming such things gives me access to knowing about tools I would not have known otherwise. I like knowing the existence of things, even if I don't recall the exact thing, since knowing that something like X exists has saved me from having to reinvent X from scratch.
















§ Conclusions


I always feel a little wrong posting this at the end of every year, since I feel that among the things I cover under "read", I've internalized some things far better than others: For example, I feel I understannd Riemannian geometry far better than I do General Relativity. I try to put up the caveats at the beginning of each section, but I'd really like a way to communicate my confidence without reducing readability.
The final thing that I wish for is some kind of reading group? It's hard to maintain a group when my interests shift as rapidly as they do, which was one of the reason I really loved the AIRCS workshop: They were people who were working on formal methods, compilers, type theory, number theory, embedded systems, temporal logic... It was very cool to be in a group of people who had answers and intuitions to questions that had bugged me for some time now. I wonder if attending courses at a larger research university feels the same way. My uni is good, but we have quite small population, which almost by construction means reduced diversity.
I also wish that I could openly add more references to repos I've been working on for a while now, but I can't due to the nature of academia and publishing. This one bums me out, since there's a long story of a huge number of commits and trial-by-fire that I think I'll be too exhausted to write about once the thing is done.
Sometimes, I also wish that I could spend the time I spend reading disparate topics on focused reading on one topic . Unfortunately, I feel like I'm not wired this way, and the joy I get from sampling many things at the same time and making connections is somehow much deeper than the joy I get by deeply reading one topic (in exclusion of all else). I don't know what this says about my chances as a grad student in the future :).