isographist

A Random and Circuitous Walk Through the Forest of Knowledge and Wisdom

I took another sabbatical from work in February. Once again, I felt as if I was getting close to burning out. I wasn't growing or learning as a software engineer, and my development as a person was stunted. LLM coding agents were eroding a core piece of my identity. Six months after my first sabbatical, I was off from work yet again with the goal of finding myself and a path forward.

Rocq

The first step of my journey was learning Rocq. The way I view it, Rocq is a kind of game where you are given puzzles in the form of mathematical theorems, and answers are proofs of those theorems within Rocq's rules. LLM coding agents bother me because of their lack of precision, and I thought throwing them at a domain that had rigorous definitions of correctness could make them more precise.

I worked through the first volume of Software Foundations, a textbook on formal verification in Rocq. After all the "impure" software I had written in the past few years, Rocq felt serene: a place where math and computers danced in harmony.

One of my favorite puzzles in Software Foundations is about Church numerals, an alternate way of defining natural numbers. A number n is defined as a higher order function that takes in a function and an element and applies f to x, n-times. For example, the number one is . The number two is . Zero is just x. Think about how addition is defined: a higher-order function that accepts two numbers n and m (which are themselves higher-order functions), and produces a higher-order function that applies f to x, n times, then m times!

After messing around with Rocq for a few weeks, I felt that it would take years of study before I got to a level that would allow me to achieve my goal. I briefly flirted with pursuing a degree, but I didn't feel passionate enough about Rocq, formal methods, or academic research to follow through. Ultimately, I think I gained a valuable tool in the toolbox, and a refreshed feeling that there is still beauty in software and mathematics.

Recommendation Systems

The next step of my journey took me to recommendation systems. For a long time, I'd flirted with the idea of building a recommendation system for e621 posts—a yiff recommendation system, or yiff RS. Users would be suggested posts in a feed-like format, and could react to indicate whether they liked or disliked the posts they were shown.

To start, e621 provides daily database exports. My initial approach was to use TF-IDF to rank posts: each post is a "document", and each tag is a "term" within that document. A user's previous likes and dislikes would build a sparse vector whose entries corresponded to a tag and whose values count the number of posts the user liked with that tag, minus the number of posts they disliked with that tag. Posts that would appear on a user's feed were ranked by the inner product of a post's TF-IDF factors and the user profile vector.

This approach had several issues. First of all, it was expensive to compute. If I recall correctly, there are ~1M tags on e621, so any operation over all of them is expensive. Second of all, using TF-IDF factors often meant that the algorithm latched on to a small handful of tags, and would only suggest posts with those few tags. If you were lucky, these tags were tags you liked, but oftentimes they were just spurious correlations.

My next attempt was based on singular value decomposition. By (1) constructing a sparse binary matrix of posts by tags, where each entry corresponds to whether a post is tagged with a specific tag, then (2) computing a truncated SVD, you're given a low-dimensional vector embedding of every e621 post. The dimensions of these embeddings correspond to high-level components. If I recall correctly, some of these components were dragons, My Little Pony, male/female, and, surprisingly, feet. A user's vector was constructed by summing the embeddings of all their liked posts, minus the embeddings of all their disliked posts. Posts were ranked based on their cosine similarity to a user's vector.

Empirically, the SVD-based approach performed better than the TF-IDF approach: using low-dimensional embeddings meant that the performance of cosine similarity search could be drastically improved with HNSW indexes, and using embeddings over terms resulted in less overfit recommendations. However, the overall performance of the SVD-based approach was still subpar. Because the user profile vector was the sum of incoherent posts, it often pushed the user's vector into an uncovered region of embedding space, resulting in essentially random recommendations. Moreover, the SVD-based approach still didn't address the exploration problem. I tried various approaches to increase the exploration, including randomly sampling which posts were summed into the user vector, and randomly amplifying various components of the user vector, but no approach produced satisfying results.

I suspect that the most fruitful approach to building a yiff RS would be to perform some sort of analysis on the post-by-favorites or post-by-upvotes matrix. Unfortunately, e621 does not provide this data in its database exports. I tried scraping this data from e621 using the API, but it would have taken months or years to get a substantial portion. In the end, it's in the hands of e621 developers to build a good yiff RS.

System Design

The third and final step of my journey took me into system design. At this point, it was about four months into my leave, and I needed to start applying for jobs again soon if I wanted to keep my health insurance. I was also afraid that I was losing the ability to even motivate myself to work at all, and that, if I wasn't able to find a job soon, it would be years before I could work again.

Across multiple jobs that I applied for, there was an unexpected focus on system design over coding. I suspect this is due to the pervasive view in the software industry that coding is a "solved problem", but for me it meant I would need to study an area of software engineering that I had little experience with.

I purchased a copy of Designing Data-Intensive Applications by Martin Kleppmann, and read it from cover to cover. If you're a software engineer working on a large system, I highly recommend giving it a read, or at least skimming the chapters that are relevant to your work. It turned over a lot of stones for me, including queues, fault tolerance, two-phase commit, and consensus algorithms such as Raft and Paxos.

What ultimately helped me prepare the most for interviews was building small-scale versions of some common system design problems. Building a mini Redis-based rate limiter taught me a lot more about Redis than reading about it. Doing these mini projects also familiarized me with Docker.

And finally, I landed a new job!

Conclusion

For the first time in my life, I've felt purposeless. During college, my purpose was to get a degree and learn the most I could. After college, my purpose was to learn about myself and find my place within the furry fandom, attend conventions, and meet new people. At my previous job, my purpose was to learn and have fun as a software engineer. Briefly, I thought my purpose resided in someone else dear to me, but, for reasons I'm not yet ready to discuss, that wasn't meant to be. Now, I'm not sure what my purpose is—what reason do I even have to get out of bed each day?

Frankly, I haven't been taking great care of myself or my belongings. I've been eating and sleeping quite poorly during this time. My room is somewhat of a mess, and there is so much cleaning I need to do. Perhaps counterintuitively, I've taken the best care of myself in the times when I'm the most stressed, maybe because the external stressor is a forcing function to get myself in order.

Right now, I'm excited and anxious to start a new job. I feel good about the position: the manager seems driven, knowledgeable, and compassionate, and my day-to-day will be working on hard but pure engineering challenges. I'm still fretting whether my ability to sustain a job has atrophied over the past five-and-a-half months, but that's just a challenge I'll have to face as it comes.