A few months ago, AI math results started making headlines. “Do a breakthrough” became a Twitter meme. Naturally, I became curious whether I, too, a math noob, can find some open mathematical problem and then have a frontier model solve it. It took me an entire month of my free time and a boatload of tokens, but I believe I’ve obtained a Lean proof of this conjecture posed by John Conway 50 years ago: Conway’s refinement conjecture claims that omnific integers have a refinement property: if ab = cd, there are integers e, f, g, h with a = ef, b = gh, c = eg, d = fh. My proof has not been…
Every single time a post about atproto hits Hacker News, somebody asks in the comments: “But where are all the Bluesky instances?”. The problem is, there are no instances in atproto! The question is a category error. Instances are a Mastodon-brained concept, and I wanted something I can link to that explains this clearly. So this is that post. RSS and Google Reader I know RSS is still being used somewhere (podcasts?!) but its heyday is arguably behind. Which is a shame. For a few years, which some of us might fondly remember as the golden age of the web, it felt like blogging was a cool…
Remember files? .doc.doc.doc.doc.jpg.jpg.svg You write a document, hit save, and the file is on your computer. It’s yours. You can inspect it, you can send it to a friend, and you can open it with other apps. Files come from the paradigm of personal computing. This post, however, isn’t about personal computing. What I want to talk about is social computing—apps like Instagram, Reddit, Tumblr, GitHub, and TikTok. What do files have to do with social computing? Historically, not a lot—until recently.…
My sabbatical is soon coming to an end, and I am looking for a new job. In particular, I am looking for a job at a company that would like to sponsor a working visa for me in Japan, where I’d like to relocate within the next year. If you can sponsor a software engineering visa in Japan and think I might be a good fit, please email [email protected]. Below I’ll recap some of my past work, with more details re: what I’m looking for near the end of this page. (Skip to the end) Past Work Hi! My name is Dan Abramov. I started programming about 20 years ago and then I couldn’t stop—so I’ve been…
I’ve been vibecoding a little app, and a few days ago I ran into a bug. The bug went something like this. Imagine a route in a webapp. That route shows a sequence of steps—essentially, cards. Each card has a button that scrolls down to the next card. Everything works great. However, as soon as I tried to also call the server from that button, scrolling would no longer work. It would jitter and break. So, adding a remote call somehow broke scrolling. I wasn’t sure what’s causing the bug. Clearly, the newly added remote server call (which I was doing via React Router actions) was somehow…
You might have heard about the AT protocol (if not, read this!) Together, all servers speaking the AT protocol comprise the atmosphere—a web of hyperlinked JSON. Each piece of JSON on the atmosphere has its own at:// URI: at://ruuuuu.de/app.bsky.feed.post/3lzy2ji4nms2z at://danabra.mov/sh.tangled.feed.star/3m23ddgjpgn22 at://tessa.germnetwork.com/pub.leaflet.publication/3lzz6juivnc2d But where do they point, exactly? Given an at:// URI, how do you locate the corresponding JSON? In this post, I’ll show you the exact process of resolving an at:// URI step by step. Turns out, this is also a…
Open source has clearly won. Yes, there are plenty of closed source products and businesses. But the shared infrastructure—the commons—runs on open source. We might take this for granted, but it wasn’t a foregone conclusion thirty five years ago. There were powerful forces that wanted open source to lose. Some believed in the open source model but didn’t think it could ever compete with closed source. Many categories of tools only existed as closed source. A Microsoft CEO called open source cancer—a decade before Microsoft has rebuilt its empire around it. The open source movement may not…
This is my opinionated syntax primer for the Lean programming language. It is far from complete and may contain inaccuracies (I’m still learning Lean myself) but this is how I wish I was introduced to it, and what I wish was clarified. Why Lean? This post assumes you’re already eager to learn a bit of Lean. For motivation, I humbly submit to you two takes: one from me and one from its creator. Declaring Definitions Let’s start by writing a few definitions. These can appear at the top level of the file: def name := "Alice" def age := 42 (Try it in the online playground.) Note you have to write…
What is the type of 2 + 2 = 4? In TypeScript and most other languages, logical expressions have a Boolean type: const question1 : boolean = 2 === 2; // true const question2 : boolean = 2 + 2 === 4; // true const question3 : boolean = 2 + 2 === 5; // false In fact, we can drop the : boolean type annotations because TypeScript can see that all of these are logical expressions—and so they obviously must be booleans: Note that question1, question2, and question3 are all of the same type. In TypeScript, there is only one boolean type, and only two values (true and false) of that type. Let’s…
For the past few months, I’ve been writing a lot of Lean. Lean is a programming language, but it is mostly used by mathematicians. That is quite unusual! This is because Lean is designed to formalize mathematics. Lean lets mathematicians treat mathematics as code—break it into structures, theorems and proofs, import each other’s theorems, and put them on GitHub. The big idea is that eventually much of the humanity’s mathematical knowledge might be available as code—statically checked, verifiable, and composable. So what does using Lean feel like? Sorry Not Sorry To give you a taste of Lean,…
Usually, when we think about build failures, we think about things like syntax errors. Or maybe “module not found” errors. You don’t want to forget to check in the files that you’re using. Better a build error now than a crash later. We can also think of a broader set of cases where we want to fail the build—even if it technically “builds”. For example, if the linting fails, you probably don’t want to deploy that build. Even if it was merged into main! If a lint rule is wrong, you can always suppress it. So failing the CI is preferable to shipping bad code. If you’re sure it’s correct, you…
It’s been a while since I’ve posted any personal/professional updates. As some of you might know, I left Meta in July 2023. I wanted to take a long break from work around then—but I got excited about Bluesky being at the intersection of all my interests (React, open source, being addicted to Twitter) and I’ve spent the next (almost) two years there. I’ve learned some of the ins and outs of React Native, helped the team get the app a lot more polished, and also did a little bit of engineering management. Then I realized I actually needed a long break, and it could not wait any further. So I…
React Server Components (RSC) is a programming paradigm that lets you express a client/server application as a single program spanning over two environments. Concretely, RSC extends the module system (the import and export keywords) with novel semantics that let the developer control the frontend/backend split. I’ve previously written about the 'use client' and 'use server' directives which mark the “split points” between the two environments. In this post, I’d like to focus on how these directives interact with the import and export keywords. This post is a deep dive for anyone who’d like to…
One of the big ideas of LISP is that code is data, and data is code. I mean, that’s kind of generally true, but in LISP it’s both culturally and syntactically emphasized. For example, let’s take this piece of code in LISP: (+ 2 2) This gives us 4. But let’s put a quote before it: '(+ 2 2) Suddenly, the result is… (+ 2 2). Uh, what do I do with that? Well, that’s a piece of LISP code. “Quoting” a piece of LISP code means “don’t actually evaluate it, just give me the code itself”. Of course, I could evaluate it later: (eval '(+ 2 2)) This gives me 4 again. That’s what I mean by “code is data”…
Do you know about Progressive JPEGs? Here’s a nice explanation of what a Progressive JPEG is. The idea is that instead of loading the image top to bottom, the image instead is fuzzy at first and then progressively becomes more crisp. What if we apply the same idea to transferring JSON? Suppose you have a JSON tree with some data: { header: 'Welcome to my blog', post: { content: 'This is my article', comments: [ 'First comment', 'Second comment', // ... ] }, footer: 'Hope you like it' } Now imagine you want to transfer it over the wire. Because the format is JSON, you’re not going to have a…
Fair warning—this one’s for the nerds. React Server Components is a programming paradigm that extends the module system to express a server/client application as a single program spanning two runtimes. Under the hood, the RSC implementation consists of two main pieces: A serializer for React trees (packages/react-server in the React repo). A deserializer for React trees (packages/react-client in the React repo). The react-server and react-client packages are internal to the React repo. They are fully open source, of course, but they don’t get published in their raw form to npm. This is…
How many requests should it take to navigate to another page? In the simplest case, a navigation is resolved in a single request. You click a link, the browser requests the HTML content for the new URL, and then displays it. In practice, a page might also want to display some images, load some client-side JavaScript, load some extra styles, and so on. So there’ll be a bunch of requests. Some will be render-blocking (so the browser will defer displaying the page until they resolve), and the rest will be “nice-to-have”. Maybe they’ll be important for full interactivity but the browser can…
RSC means React Server Components. And yet, although this blog is built with RSC, it is statically served from a Cloudflare CDN using their free static hosting plan. It costs me exactly zero. Zero. How is this possible? Aren’t these React Server Components? In the past, “server” and “static” frameworks were thought of as separate tools. For example, you might use Rails or PHP for a “server” app, but if you wanted to generate a “static” HTML+CSS+JS site, you might use Jekyll or Hugo instead. However, it’s getting more common for frameworks to support both “server” and “static” output modes.…
Okay, so in Astro you have two things: Astro Components: They have the .astro extension. They execute exclusively on the server or during the build. In other words, their code is never shipped to the client. So they can do things that client code cannot do—read from the filesystem, hit the internal services, even read from a database. But they can’t do interactive things aside from whatever exists natively in the HTML or your own <script>. Astro Components can render either other Astro Components or Client Islands. Client Islands: Components written for React, Vue, and so on. This is your…
Here’s a piece of HTML: <html> <body> <p>Hello, world</p> </body> </html> Imagine this was the only piece of HTML you’ve ever seen in your life. If you had complete freedom, which features would you add to HTML, and in what order? Where would you start? Server Tags Personally, I’d like to start by adding a way to define my own HTML tags. It doesn’t need to be complicated. We can just use JavaScript functions: <html> <body> <Greeting /> </body> </html> function Greeting() { return <p>Hello, world</p> } To make this work, let’s specify that when the HTML is sent over the network—that is,…
Read at the source
Your visit, your choice.
Optional Google Analytics helps us understand visits. Microsoft Clarity records masked interactions to improve the site. Optional tools stay off unless you choose them. Privacy details.