◇ Different Dimension Fathomings (Fall 2025 Edition)

◇ Multi-Core By Default (Ryan Fleury, 2025)

This article introduces an idea I never thought about — shader-like programming on the CPU. While this might not be universally applicable to every kind of programming³, it’s a match made in heaven for certain projects of mine (i.e. my game). I’ll definitely give this approach a go in the future. If nothing else, it’s definitely changed the way I think about multi-threading!

◇ Without the futex, it’s futile (Lee T. H., 2025)

I was already familiar with the public API of futexes, and had a rough idea about how one would go about implementing higher order primitives on top (I had read through the relevant sections of Odin’s standard library), but this article answered a lot of the questions I had regarding the finer details of using futexes in practice.

◇ Making Sense of Acquire-Release Semantics (Dave Kilian, 2023)

The previous article still left me with some questions. I kept seeing the “acquire”/“release” thingies while reading Odin code, and had always been a bit confused about their meaning. Both Odin’s and Rust’s standard libraries do a pretty terrible job at explaining what those things do (in retrospect, they are pretty close! All that’s missing is an additional paragraph containing some background information, but I digress). I still won’t claim to be proficient at thinking about atomics, but this article has at least made me a bit more aware of the things I don’t know, hence things that I can learn. This also means I’ll be a bit more willing to experiment with atomics in my own code.

◇ The current technology is not ready for proper blending (Clément Bœsch, 2025)

It’s not like I hadn’t heard about sRGB vs linear blending, but the visual comparisons with OkLab were super informative, and something I’ll keep in mind for my game.

◇ Please write (riki moe, 2025)

I’ve read the post multiple times over the past weeks — it’s what motivate me to finish writing up about the site’s refactor. There’s not much I can add here — the article didn’t present anything I didn’t previously know. It’s just a nice reminder I need to get in the habit of writing more.

◇ Organizing your Nix configuration without flakes (Kylie McClain, 2025)

I had already read Jade’s post on npins, and have had my fair share of annoyances with flakes. This post tackles some of the more organization-related questions I haven’t taken the time to solve for myself. I will soon try the no-flake approach for some smaller projects, and report back. I might one day even migrate my dotfiles away from flakes, although I really don’t have it in me to refactor my whole nix setup right now.

◇ memory fades but our words are forever (Kylie McClain, 2020)

This article made me reflect on my own usage of Discord. Over the past seven years, I’ve sent over 250k messages in a small server I’m a part of. I have people I’ve delivered over 70k DMs to. I’ve sent over 40k messages in 2025 alone⁴. Yet even after having spent so much time together, I can’t say I particularly enjoy Discord (the platform).

At first, I took issue with their hostility towards user theming and alternate clients. Then, I started being a bit annoyed about how RAM-hungry their desktop app can be, all while providing a terrible user-experience while on unstable internet.

I do not like the myriad of micro-transactions that have over-time infected the app. I remember my 9th-grade self thinking I’d buy Nitro (the platform’s paid subscription) the moment I have a stable job, not for the perks themselves — but to support the platform I had grown to love. Years later, and buying Nitro would feel like throwing money at a company that’s going in the exact opposite direction than what I had hoped.

Of course, these are but symptoms of the deeper issue that is Discord’s business model. Few commercial chat applications can last as much as Discord has, especially considering its scale — it’s an impressive feat, no doubt. But the experience of lasting that long has morphed the platform — a trial by fire of sorts.

Nonetheless, the article discusses the technical aspects in much deeper details. I have (in the past) backed up a few small Discord servers. The linked piece will hopefully motivate me to get back to work and back up some of the places I truly cherish.

I grew up on Discord, ever since the age of 13 or 14 (the time I got my old, barely held together laptop). I met many great people (a surprisingly large chunk of whom I’ve since met in person), yet I’m not sure whether the platform has changed me for the better or for the worse. Time will tell, I guess. It’s wild to imagine how I’ll look back at the hours spent on the silly blurple chat platform a few decades from now. Only time will tell…

If you want to talk to me, send me a message anywhere, be it on IRC, Matrix, Signal, or even Discord (if you must) — I even enjoy email!

◇ Violating memory safety with Haskell’s value restriction (Alice, 2025)

The article starts by discussing why Haskell doesn’t need a compiler-supported value restriction to prevent creating polymorphic references. So far, everything should feel like common sense to anyone who’s written any non-trivial amount of Haskell. The interesting twist comes in the second half of the piece, where the issue is forced back into the language by unwrapping IO’s internal representation. I didn’t even know this (unwrapping IO) was possible before! The (unsurprising) lesson is that you really shouldn’t unwrap IO, even if the State# tokens are handled linearly.

◇ The intrinsic topology of a Martin-Löf universe (Martin Escardo, 2012)

This one’s super interesting! The page begins by defining a notion of “convergence” of sequences of types. This is achieved by recalling that a sequence $x:\mathrm{\mathbb{N}}\to X$ converges to some $x_{\infty }$ precisely when there’s a sequence $x\prime :{\mathrm{\mathbb{N}}}_{\infty }\to X$ that sends the naturals to $x$ and $\infty$ to $x_{\infty }$.

But how is ${\mathrm{\mathbb{N}}}_{\infty }$ even defined in the underlying type theory? Of course, $\mathrm{\mathbb{N}}$ itself can easily be defined as an inductive type (indeed, this is often used as an example for introducing the notion). But how would we go about taking the 1-point compactification of this type? The project the linked article is part of (TypeTopology) defines ${\mathrm{\mathbb{N}}}_{\infty }$ as the type of decreasing sequences of booleans. This is still a bit obtuse, but it essentially means elements of ${\mathrm{\mathbb{N}}}_{\infty }$ can either be sequences of finitely many ones (i.e. 1111111100000...) or the unique sequence of infinitely many ones (1111111...).

One might wonder how this differs from $\mathrm{\mathbb{N}}+1$. Intuitively, one can trivially construct a map $\mathrm{\mathbb{N}}+1\to {\mathrm{\mathbb{N}}}_{\infty }$, yet the reverse is not possible without some kind of oracle that can distinguish $\infty$ from the rest of the sequences. Put another way, equality on ${\mathrm{\mathbb{N}}}_{\infty }$ is not decidable⁵.

Put in very informal⁶ language, the main proof in the article goes like this:

1. The attach-① construction (and the related lemmas) allow us to show that ${\lim }_{n\to \infty }{X}_n=\mathrm{𝟙}$ for any $X_n$.
2. In particular, we have ${\lim }_{n\to \infty }⌀=\mathrm{𝟙}$.
3. Multiplying both sides by some $Y$ shows that ${\lim }_{n\to \infty }⌀=Y$, since $⌀\times X=⌀$ and $\mathrm{𝟙}\times X=X$.
4. Applying the negation function⁷ to both sides of (2) yields that ${\lim }_{n\to \infty }\mathrm{𝟙}=⌀$ (since $\neg ⌀=\mathrm{𝟙}$ and $\neg \mathrm{𝟙}=⌀$).
5. We can again multiply both sides by some $X_n$ to show that ${\lim }_{n\to \infty }{X}_n=⌀$.
6. Pointwise addition of (3) and (5) shows that ${\lim }_{n\to \infty }{X}_n=Y$ (since $⌀+X_n=X_n$ and $Y+⌀=Y$).

This works for arbitrary $X_n$ and $Y$, letting us conclude that any sequences of types converges to any other type, hence universes of types have the indiscrete topology. Awesome!

◇ An RNG that runs in your brain (Hillel Wayne, 2024)

The title says it all — the article discusses an interesting class of algorithms for generating pseudo-random numbers in your brain. There’s not much to say other than the article motivating me to memorise the multiplication table for $18$ :D.

◇ What is cosh(List(Bool))? Or beyond algebra: analysis of data types. (Nikita Danilov, 2025)

Manipulating algebraic data types symbolically, be it in funky ways, is not a new idea — nor is taking a type’s derivative. Yet, the linked article goes surprisingly further than any other piece I’ve read, tackling things like the logarithm of a type, hyperbolic trigonometric functions, and more.

A fun takeaway is that bags/multisets (the free commutative monoid) are in a sense more natural than lists, corresponding to the exponential function. Indeed, it turns out multisets have nice properties like being their own derivatives.

◇ 1001 Representations of Syntax with Binding (Jesper Cockx, 2021)

I have recently come across Debruijn indexes and levels, and why they’re handy (Blueberry Wren, 2025), which mentions co-de-Bruijn indices (see Everybody’s Got To Be Somewhere (Conor McBride, 2018)) towards the end. While not the most practical approach to naming, co-de-Bruijn indices are a super cool way of handling names, which I first learnt about in the post this section is titled after. I had already read the post in question a few months ago, but this made me revisit it, and what can I say — it’s as good as I remembered it.

If you have any interest in the different ways variable naming can be represented when developing a language, then I highly recommend giving this a read. Well, you’ll probably still end up using good-ol’ de Bruijn indices/levels, stringy names, scope graphs, or perhaps HOAS, but it’s an interesting read nonetheless.

For those not familiar with the topic, this is about representing names when implementing programming languages. There’s many pros and cons to the different approaches, but the aforementioned articles do a better job at explaining that.

At a very high level, the idea with de-Bruijn indices is that binders (i.e. things that introduce variables into scope — think a lambda’s argument, or a let-statement) need not contain any name data, they simply bind “something”. Variables can then reference those binders by simply specifying how “far away from them” the binder in question was. For example, a variable holding the index $0$ references the innermost binder surrounding it, and a variable holding the index $2$ references the third innermost binder surrounding it. As an example, the function $a\mapsto b\mapsto a$ would be represented as $\lambda \lambda 1$.

De-Bruijn levels work similarly, with the sole difference being that counting now starts at the outermost binder. That is, a level of $0$ represents the binder furthest away from the variable in question. De-Bruijn indices are usually preferred as they are quite “local” (for example, they allow us to wrap the expression in new lambdas without modifying anything), although de-Bruijn levels have their uses too (they are, in a sense, stable with regards to substitutions). With de-Bruijn levels, the $a\mapsto b\mapsto a$ function above would be represented as $\lambda \lambda 0$.

Co-de-Bruijn indices, as the name suggests, are the supposed (more on this later) dual of the aforementioned de-Bruijn indices. Instead of binders holding no information and variables doing all the work, co-de-Bruijn indices flip the script on its head — now variables hold no information, and binders do all the work… except not really? The way this works is that each expression keeps track of the number of variables it uses. All variable expressions use precisely one variable (by definition). Call expressions not only track the number of variables used by the caller and callee, but also track which of the total amount of variables are used on both sides. All a lambda needs to track then is whether the variable it introduces is used or not.

Ok, my explanation wasn’t the best — go read the articles I listed, they’re so much better. It’s also clear that you would never use co-de-Bruijn indices in practice — keeping track of covers for every single function application seems horrible, and would scale terribly when it comes to memory usage. Still, it’s very interesting to think about conceptually, it almost feels… magical. We are not only not using any names to represent things, but don’t even need to index into some outer context. Indeed, it feels like every constructor for the AST keeps track of precisely how the variable usage flows from its children to the larger structure.

Still, I couldn’t shake this feeling that the function application constructor is doing all the work. Shouldn’t the lambda constructor be where this is all happening? This lead to me coming up with the following construction (see the full source, which also contains a simply-typed version of the concept):

-- A binary sequence of length k containing l 1s
data Filter : (k l : ℕ) → Set where
  done :              Filter      0       0
  yes  : Filter k l → Filter (suc k) (suc l)
  no   : Filter k l → Filter (suc k)      l

data Term : ℕ → Set where
  var  : Term 1
  app  : Term k → Term l → Term (k + l)
  -- Each variable filtered out by the sequence is bound here
  lam  : Filter k l → Term k → Term l

The idea is simple:

• terms are indexed by the number of unbound variables therein
• variable expressions contain precisely one such variable (by definition)
• applications sum the number of unbound variables on each side
• lambdas filter out the unbound variables by specifying which variables to bind

This is obviously horrible in practice, but here’s some example usage:

-- λ0
identity : Term 0
identity = lam (no done) var

-- λλ1
const : Term 0
const = lam (no done) (lam (yes done) var)

-- λλλ201
flip : Term 0
flip = 
  lam (no done) (
    lam (no (yes done)) (
      lam (yes (no (yes done))) (
        app (app var var) var
      )
    )
  )

I’ve contacted the author of the article, and we’ve had a nice conversation about it. The takeaway seems to be that this technique is new, but not particularly pretty in practice. I don’t think the original co-de-Bruijn indices are particularly useful either, hence my goal has been achieved.

◇ Needy Programs (Nikita Prokopov, 2025)

This is a short & sweet article about how modern apps rely on features like accounts & notifications more often than they should. I particularly enjoyed the mention of Syncthing & Mullvad as examples of apps that do synchronization and payments respectively without involving the idea of accounts — a reminder that this is possible, one that I’ll keep in mind for my future apps.

◇ Making a Language (Ethan Smith, 2023–present)

The internet contains many resources on language development. While I haven’t learnt much new from the (on-going) series herein, I think this is a wonderful resource for people new to the topic, especially those interested in type theory and the like.

◇ The mathematical past is a foreign country (Mark Dominus, 2025)

The article presents a wonderful example of how many implicit practices are baked into our modern mathematical understanding. In particular, the piece highlights the way earlier understandings of the Peano Axioms overload the addition operator to refer to both the successor function (in the case of $a+1$) and natural addition itself otherwise.

◇ Fizz Buzz with Cosines (Susam Pal, 2025)

The name says it all — one can solve the Fizz Buzz problem using trigonometric functions, isn’t that awesome?

◇ Error Codes for Control Flow (Alex Kladov, 2025)

Zig has built-in support for errors-as-values, yet said errors are represented by a numerical error code and nothing else — there’s no payload to carry additional data! I found this quite odd when I was first learning about the language a few years ago, but I eventually understood what they’re going for. The article at hand does a good job motivating this decision.

The base idea is that error codes signify whether something went wrong, and what. Additional error data can be propagated through side channels, like buffers passed in as arguments. The advantage of this approach is that the caller has control over whether the additional data is needed — it can simply pass in a nil buffer if that’s not the case!

I haven’t used this approach in practice (I don’t use Zig for much), but have interacted with C libraries that use this kind of approach (it’s not like you have much of a choice when using C), so I do see the appeal.

◇ in defense of a faceted self (small cypress, 2025)

For years I have struggled with being myself around others and not wearing metaphorical masks, and this is something I am still working on. This article talks a bit about the other extreme, and about situations where being “faceted” is not a bad thing.

◇ ADHD and agency (small cypress, 2025)

The name is pretty self-explanatory. I’m not a person who has ADHD (I mean I could, but I’m not the kind to self diagnose), yet the discussion around agency applies to other areas of life as well.

◇ People’s appetite for forgiveness (Blueberry Lemonade, 2025)

The article talks about the way people in fiction view forgiveness, the way real people view forgiveness in fiction, and the way real people view forgiveness in the real world. I won’t do much talking about the article itself (go read it yourself!), but I will provide some anecdotes regarding the way certain stories handle forgiveness.

One show the article mentions is Avatar: The Last Airbender. I do think the ending fits the themes of the show⁸, but I can’t help but feel like it does that in spite of the prior actions of its characters. Aang is never shown outright killing someone, but there’s many scenes where I thought that was implied. He’s blown groups of soldiers off cliffs before⁹. There’s just… no way they’ve all survived. I don’t know, this is why the ending took me out for a while. It’s a good ending — but it requires one to forget some past scenes for it to be thematically relevant.

An example the article has not brought up is One Piece¹⁰. One could write many pages about Luffy’s relation to justice (I’m sure there’s many (video) essays about it out there already), but the short of it is that he… doesn’t really care about it; not directly at least. He breaks some of the world’s worst criminals out of prison for no other reason than having them help him save his brother. Does that let them out and about in the wild after the fact? Sure, but who cares I guess.

Luffy does lots of just things throughout the story, yet justice is far from his direct motivation. Luffy saves entire kingdoms on numerous occasions, yet his motivation usually stems from the oppressive regimes therein hurting one of his friends.

I guess Luffy has this superhuman ability to just “sense” people’s nature, to know when they are worth forgiving, and to know when they’ve changed.

I don’t think this would necessarily work in the real world (I mean, what am I even saying — it wouldn’t), but I do find Luffy’s stance on those things quite unique among the various shows that tackle the issue.

Also no way, I’m just now learning the author works for 7th Beat Games????? I love their games OMG, the world is so small sDFJslkdjflskdjf

◇ The phone saga

This is a series of multiple articles about escaping one’s phone usage.

◇ Parting thoughts

This has been one hell of a journey, hasn’t it? It’s crazy to think I wrote this much even though I only really started working on this around the end of October. I think further installments of this series will come out monthly (otherwise they’d get quite large), although that’s something for future-me to figure out.