Latest Posts (20 found)
Unsung Today

“They take one look at the UI and abandon it.”

Hiding inside this page on “user-driven UI” by Brad Woods are two useful things. The first is the concept of “zone of proximal development.” The idea, as I understand it, is that possible tasks you face span a few categories: The space between these things is a zone. A good book or a teacher would help you navigate the zone, by giving you tasks hard enough that they will expand the zone, or even teach you how to expand it on your own – but not too hard so that you give up in failure and frustration. Woods argues that this doesn’t just apply to traditional classroom teaching, but also software, where the role of the teacher is taken by things like: The second thing was this quote by Anthony Hobday, who made a few appearances on this blog : I think this is brilliant and spot on. I always knew the creators of an app would have a problem of not seeing complexity creep in, but this made me consider that the app’s early users might also be biased the same way, and not exert much pressure. If you are familiar with an app, armed with your desire paths and motor memory, you have a lot of capacity to just ignore new menu items, new panels, and new complexity – provided it doesn’t get in your way. New AI option? Turn it off. New tab? Never click on it. New alternate way of doing things? Just continue with the old way. But as a new user, you don’t have that history, or that experience-backed confidence that a bunch of stuff can simply be ignored as it’s not crucial to everyday operation. Add to this the industry’s perverse incentives that often present new additions as the most important ones , and it’s much harder to make a sense of it all as a newcomer. And all the while, the creators and existing users might not see the problems you do. stuff you already know how to do, stuff you can learn to do on your own, stuff you can learn to do with assistance (e.g. from a teacher), stuff you simply cannot do or imagine doing. onboarding walkthroughs, progressive disclosure, help menus. Simple product is released Lots of people use it every day More features are added It’s now complicated But most people learned the basics when it was simple, so they don’t notice that it got complicated.

0 views

Multipage

Just noting Mat’s Multipage Version zine rules. I bought both issues right away. It’s weird, it’s funny, it’s a work of art, and you might even learn something. The page that is a spliced version of Marc Andreeson proposing the IMG tag in HTML with all his recent crazy shit about how he “has” zero introspection is, as previously mentioned, a work of art.

0 views

FBI Arrests Founder of Ransomware Negotiation Firm

Agents with the Federal Bureau of Investigation (FBI) on Thursday arrested the co-founder of a Canadian cybersecurity firm in connection with an investigation into the ShinyHunters hacking group that recently relieved the FBI of sensitive data on thousands of agents, multiple sources tell KrebsOnSecurity. The New York Times reported today that the FBI has arrested a Canadian man in Pennsylvania on suspicion of assisting ShinyHunters. The Times story did not identify the man, nor did a statement on Twitter/X about the arrest from FBI Director Kash Patel . One source close to the investigation told KrebsOnSecurity the Canadian person arrested this week was visiting Pennsylvania for a cyber insurance conference, and that the suspect’s company specialized in handling ransomware negotiations with cybercrime groups. Another shared that control over the ShinyHunters investigation has been centralized at an FBI field office in Texas. An online search reveals the Cyber Risk Summit was held at the Loews Philadelphia Hotel between Oct. 5 and Oct. 7. The conference had several sponsors, but according to the summit’s website its biggest sponsor was a Canadian security company called Cypfer . According to LinkedIn, Cypher was co-founded by a Canadian man named Edward Dubrovsky , who is now associated with another Canadian security firm called CyberSteward . In a post to LinkedIn approximately one month ago, Dubrovsky said he had plans to attend the Cyber Risk Summit with the rest of the CyberSteward team. Edward Dubrovsky’s LinkedIn profile. “Looking forward to continuing conversations around strategy & compliant driven coercive (ransomware, extortion) advisory, negotiations and settlement services that are global and truly agnostic,” Dubrovsky wrote. Federal court records show that on October 8, an Edward Dobrovsky (note the slight misspelling of the last name) was arrested in Pennsylvania on cyber extortion and conspiracy charges. Several of those documents — including the core complaint — are now sealed. But a handful of them were indexed at Courtlistener.com , including a summary of the complaint, which charges the defendant with “conspiracy to threaten to impair the confidentiality of information with the intent to extort money,” and “interference with commerce by threats.” Image: Courtlistener.com The inmate locator at the U.S. Bureau of Prisons website reports that a 54-year-old Edward Dubrovsky is currently being held at a federal facility in Philadelphia. But the court records indexed by CourtListener include a notice filed on October 9 that moved the case to the Eastern District of Texas, which sources say is now the epicenter of the FBI’s ShinyHunters investigation. The FBI declined to comment for this story. Dubrovsky’s LinkedIn profile states he is the author of Cyber Extortion Strategic Response , a 252-page book that promises to “take readers beyond the ransom note and into the decisions that determine how an organization responds, recovers, and protects what matters.” Edward Dubrovsky’s book, which centers on the intricacies of ransomware negotiations. “At the heart of the book is a critical distinction: communicating with a criminal is not the same as negotiating a payment, and negotiating is not a commitment to pay,” reads an excerpt from the book’s listing on Amazon. “Engagement can serve other objectives, including testing claims, gathering information, creating time, and preserving options while the organization evaluates its next move.” Mr. Dubrovsky could not be immediately reached for comment. KrebsOnSecurity also sought comment from the other co-founder of CyberSteward, and will update this post in the event they respond. The available court records in Dubrovsky’s case show that he does not currently have an attorney and has yet to be appointed a public defender by the courts. ShinyHunters typically uses phishing and stolen credentials to siphon data from corporate accounts at software-as-a-service companies, and then threatens to publish the stolen data online unless a ransom demand is paid. According to the FBI, the group has extorted more than $70 million from victims so far this year. Sources tell KrebsOnSecurity the FBI has been poring over devices that were seized last month when the Dutch police arrested the convicted cybercriminal Pepijn van der Stap in connection with the ShinyHunters investigation, and that charges against principals at other companies that specialize in ransomware negotiation may be forthcoming. Immediately after Van der Stap’s arrest, another member of ShinyHunters named “ Rey ” assumed control over the group and began taunting the FBI over data the group stole from the agency’s online recruitment portal, which included each’s person’s unit and specialization, as well as medical and psychiatric records. Last week, Reuters reported that Rey — identified as a teenager named Saif Al-din Khader — had been detained and was cooperating with FBI investigators. On October 7, we detailed how Rey was apprehended as the cybercrime group allegedly sought to extort a navigation and digital aviation unit that was divested by Boeing in late 2025. This is likely to be a fast-moving story. Updates will be noted along with timestamps.

0 views

Software's centaur age may last decades

We are currently living in the age of centaurs (2022-20??). Right now, human engineers paired with AI coding systems are more effective than either by themselves. For future generations of software engineers — human or otherwise — this will be the most significant fact about the current period. As in chess’s own centaur age, people are always ready to claim that the centaur age is over and the age of AI supremacy has begun. But the age of centaurs in chess lasted about twenty years, and previous centaur ages have lasted far longer . This should be encouraging to many of us. If software engineering goes along similar lines, we may be able to ride it out another decade or two: enough to make serious plans about what comes next, or to finish out our careers entirely. It began with GitHub Copilot, which launched in 2022 as AI-powered autocomplete. A confident engineer who knew exactly what they wanted could tab-complete their way through lines of code and sometimes entire functions. Being able to chat with language models like GPT-4 provided the next upgrade. Although the models would still get things wrong, it was helpful to have a generalist on tap for areas that were a complete mystery. Coding agents rose to prominence with Cursor’s “agent mode” in 2024 and Claude Code in early 2025. Early agents needed close supervision to prevent them from going off the rails, but were still helpful to automate straightforward tasks. Current agents — after the November 2025 release of Claude Opus 4.5 — are reliable enough to run entirely unsupervised. Their output still needs human review, but the kind of mistakes they make are more mistakes of alignment than regular bugs: not matching the organization’s technical values, over-engineering certain areas and under-engineering others, deciding where to spend effort, and so on. It is no longer possible to credibly argue that an unassisted software engineer can beat a centaur team. The value provided by coding agents is just too great: not just the speed of producing code, but the speed of review and testing. However, we are not yet at the point where an unsupervised coding agent can beat a centaur team either. All the impressive work I’ve seen from LLMs has had a competent human software engineer in control. Centaurs are on top. Would we expect our centaur age to be shorter? On the one hand, chess is a much simpler problem than software engineering, and is more amenable to learning methods like self-play. On the other hand, software engineering is massively more lucrative to solve, and many orders of magnitude more funding is being plowed into the problem than was with chess. On the third hand, “solving” software engineering means creating much more software, which increases the total work-to-be-done, so even if the relative human share of that work is shrinking, the overall amount of human work might grow. On the fourth hand, the level of generally-capable AI needed to address software engineering will have huge effects on other fields, the ripple effects of which are likely to negatively impact software engineering jobs (for instance, crashing the economy, widespread social unrest, and so on). On the fifth hand, we might think that chess had an unusually fast centaur age. Previous centaur ages lasted much longer. In knitting, where a human and a knitting-frame could outcompete any hand-knitter, the centaur age lasted two hundred years . On the sixth hand, technological change is moving ever faster . I could probably find a seventh, eighth, and ninth hand if I wanted to 1 . But overall I think we have no real idea of how this is going to turn out. Chess is the most recent example of a centaur age we have, and it’s attacked by the same AI-based forces of automation as software is. It’s thus reasonable 2 to make a default assumption that the length of software’s centaur age will be similar to chess’s. Suppose I have convinced you that human-AI partnerships will be the dominant force in software engineering for at least the next decade. What then? Don’t quit! Don’t give up on software engineering and go become a carpenter, or open a cafe, or try to get a retail job. Unless you are somehow really, really passionate about doing those things, it is going to suck : unrewarding, grueling work that you are not good at. A decade of software engineering work is long enough to take your time and think seriously about your next steps. Lean into the partnership. A guaranteed way to fail in a centaur age is to refuse to become a centaur. The idea that AI is a passing fad was a reasonable position to hold in 2023, but we’re way past that now. The AI financial bubble popping will not mean the end of AI . It’s here to stay. Think hard about what value humans can still add. This is going to change over time, and getting it right is the difference between being an effective (and employed) centaur and being a meat proxy . In 2023, technical expertise was the primary source of human value. Today, I personally think it’s going to come down to alignment , but this is still early days. I’ve also seen arguments for taste, though it’s hard to define that non-circularly. We need a lot more engineers thinking through this problem. It’s a common fear response to try and skip ahead to the worst-case scenario. But those of us working in the age of centaurs should avoid that. We need to think about how the job of software engineering functions now , not how it might function in twenty years when AI has completely transformed the landscape. People are too quick to declare that we’re in the software engineering apocalypse. We can certainly see it from here, but we’re not there yet. The spectre of full automation can loom on the horizon for decades. If you panic and jump ship early, you could be giving up on an entire normal-length career. Maybe: AI as fundamentally different technology; diffusion of even radically better technology is slow in practice and bottlenecked by organizational friction; human software companies will get outcompeted? I don’t really know what I think about these arguments. This move should be familiar to anyone with a philosophy background. If you have one argument and one counter-argument, the most recent counter-argument is probably right. If you have a stack of arguments and counter-arguments going back a thousand years, the most recent counter-argument should be treated with suspicion: better to take in the whole debate holistically and judge which side is more compelling to you. Maybe: AI as fundamentally different technology; diffusion of even radically better technology is slow in practice and bottlenecked by organizational friction; human software companies will get outcompeted? I don’t really know what I think about these arguments. ↩ This move should be familiar to anyone with a philosophy background. If you have one argument and one counter-argument, the most recent counter-argument is probably right. If you have a stack of arguments and counter-arguments going back a thousand years, the most recent counter-argument should be treated with suspicion: better to take in the whole debate holistically and judge which side is more compelling to you. ↩

0 views

A tale of four theorem provers, or: A (reasonably) opinionated comparison of Isabelle/HOL, Lean, HOL4, and Agda

In which I compare Lean, Isabelle/HOL, Agda, and HOL4 with only mild regard for "fairness". All four of the above are theorem proving applications; that is, their purpose is to computer-formalize mathematics. Broadly speaking, both Lean and Agda are dependent-types based systems, utilizing the Curry-Howard correspondence to prove theorems via a complex type system, whereas Isabelle/HOL and HOL4 are LCF-style systems, with a small "proof kernel" containing base rules (e.g. ) that all proofs must be constructed via. Both foundations have advantages and disadvantages, and some will be discussed. I have formalized in all four a proof of the infinitude of primes; that is, the statement "For any number n, there is a prime larger than n". The exact proof formalized is the "usual" construction by Euclid, which you can find on Wikipedia if you want; see here . All of the proofs structurally look similar (mostly, we'll get to that), and hence it was the user experience that made the difference. For transparency, before this experiment, I was most familiar with Isabelle/HOL and Agda, and to some extent learnt HOL4 and Lean as part of this review. What follows is a bunch of opinions and somewhat arbitrary categories. Don't expect an unbiased review, please. If you only want proof comparisons, skip to Proof Comparisons, and if you only want more opinions, read the below and then skip to Arbitrary Rankings. The opinions go first. I do not claim any of the following proofs are perfect! They're probably quite mediocre, really. There are a few categories by which we can group these theorem provers. We have the above mentioned: But there's also: Reasoning: Both Isabelle/HOL and Lean provide "live updates" as you type, and their structured proofs can be "down-arrow"'d through, to see intermediate steps. In contrast, both completed HOL4 and Agda proofs exist as fully-put-together terms that must be manually taken apart if you wish to inspect their internals. Both HOL4 and Agda can show you your current state and related information at any time, of course. Isabelle/HOL has , which calls out to a number of external proof generation methods (SAT/SMT solvers, various FOL solvers, etc). For any goal that looks doable-but-annoying, there's a solid chance can solve it - this is nice because it saves you work, but the proofs it generates are also indecipherable, which is perhaps less than ideal. There also exists an equivalent for HOL4 called HolyHammer, but I didn't realize it existed until after I was writing this. Oh well. Isabelle/HOL and HOL4 both have very good support for many automated simplification and proof methods, which come in quite handy when trying to work with complex assumptions, for example. It may not be obvious how to proceed without simplification kicking in to chunk everything down. Lean has decent automation, but not to the same level as Isabelle/HOL or HOL4. Its is not nearly as productive, and while is a very neat approach that can sometimes rival , a lot of the time it's quite useless for reasons beyond me. Both and are all-or-nothing; if they don't solve the goal, they make no progress. This is in contrast to (in all three), or more specialized tools like (Isabelle/HOL) or (HOL4), which can make some progress and then leave the context in (ideally) a better place. The fact Lean doesn't have nearly as good partial-automation is a bit of a shame, because in my experience that's what actually matters more. Notably, both Lean and Isabelle/HOL have a (In Isabelle/HOL, / for with/without ; in Lean, / / ) that "have a go" at your goal with various automated methods and direct solve attempts. HOL4 doesn't have an equivalent, as far as I can tell, which is unfortunate, as it's quite handy. Agda has essentially no automation. The only simplification you get is what can be computed based on inputs to functions. This, to be a bit frank, sort of sucks. It's quite hard to get things done because there's so much manual fiddling that must be taken into account. I am personally not a fan. Isabelle/HOL and HOL4 are both extremely classical in their foundations, which means that they accept the Law of Excluded Middle (∀ P. ¬P ∨ P), and both also axiomatize Hilbert's epsilon, which leads also to the Axiom of Choice. This seems to have a very positive effect on automated solvers, which quite often rely on laws such as double-negation elimination (¬¬P --> P), which is equivalent to the LEM. Lean is theoretically constructive (and hence does not have the LEM by default), but some of the "good" proof automation requires the LEM, and it seems the norm to use Lean classically, so that's what I did. for example just assumes you're using it. This does have the disadvantage that Lean isn't as good at dealing with e.g. existentials, for example. Agda is constructive by default, and it seems the norm in the Agda world to keep your proofs that way, so I did. The big advantage of this is that after proving there are infinitely many primes, I can actually generate them! I can give my proof a number, and it'll spit out a prime bigger than that number. The disadvantage is that it is horribly slow to do so: This may make sense if you looked at the proof structure above; we consider , so inside that proof, it's checking primality at numbers around ~360,000; that's going to be a bit slow. This construction, it should be noted, isn't meant to be fast, but it's also the most natural one. Is it worth giving up the LEM and good proof automation? You decide. I'm more a fan of LCF because it seems more amenable to automation, and I don't see the point of carrying around proof terms (classical logic is too useful!). If you vehemently disagree, email me at contact AT blueberrywren.dev, and if I like your argument enough I'll post it here. Both Lean and Isabelle/HOL are interacted with interactively. Lean has modes for other editors, but high recommends the use of VSCode, and Isabelle/HOL has its own editor (jEdit) that it also practically forces the use of. This is fine ; I understand why they do this, as interactive development is reasonably hard to make generic. Both of them make it work. HOL4 is interacted with via either an Emacs mode or a Vim mode, and keybinds that allow one to copy text in/out of a running HOL4 REPL. This sounds weird because it is, but it works surprisingly well. I was already an Emacs user, so nothing really changed for me. Agda is also interacted with via an Emacs mode, but everything happens in your file; you can use keybinds to refresh the state, add proof goals, etc. It also works fine. As mentioned above, the advantage of the Lean/Isabelle/HOL approach is that one can see proofs in-progress, which you can't with Agda. Both Isabelle/HOL and HOL4 have extremely good mechanisms for searching for theorems; an editor panel + for the former, and / for the latter. These allow for the searching of theorems by both name and by patterns, so I could for example search for lemmas of form . This is so handy! Very often you know the shape of something you want, but maybe not the lemma itself. Lean has leansearch and loogle, which are interesting, but they: Which kind of sucks. and exist as "here's stuff you might be able to do", but they're nowhere near as flexible. Agda, as expected perhaps, does not have an equivalent. One must become a master of zen looking through the right parts of the Agda standard library. Note: This isn't really meant to be a tutorial for any of these, though I will do a little explaining at the start. It's mostly for the reader to compare them, and see what ~equivalent statement proofs look like in different languages. Let's get into the proofs! We'll go segment by segment, exploring sections of the proof and explaining as we go. Before that, some vaguely interesting stats: These are nowhere near apples-to-apples, but they're still fun. We start with defining divisibility. In Agda we cheat and use the standard library version, so we can get proofs around computing divisors, which I didn't feel like redoing. Isabelle/HOL: Agda (looks like, in the standard library): So, basically the same. Then there's a few lemmas around divisibility proved ( , , etc). One we'll show off is , as it's mildly interesting in some of the theorem provers. In all of the following, the mult/sub lemma essentially states . Isabelle/HOL: The proof search procedure does most of the work. We do some unpacking, then identify as the other term (such that ). Then grind with the appropriate lemma gets us there. Like Isabelle/HOL, when supplied with the appropriate lemmas, takes it out. Very similar. is an abbreviation for , and like in Lean, we must manually point out . It was interesting to me that the Lean proof was, to some extent, such a pain. I had to put more effort into that one than any of the others, despite Lean having reasonably decent automation! Finding the appropriate lemmas was mildly more painful, and this was while I was still puzzling over syntax, to be fair. We next need to define the product of a list of numbers, which looks like the following: Isabelle/HOL: The and markers were meant to help the automated proof methods out, and they did! Defining things in HOL4 is a little interesting, because you're just defining the body as a proof! That definition spits out a theorem that is literally Here in the Agda proof we also do a bunch of work to set up what will become a decision procedure for primality. This is because later we wish to ask "Is this prime?", and without the LEM to say "It must either be prime or not prime", we need to write an algorithm to decide this for us. Back on track, we need to show a few lemmas around with prod list function. One of the interesting ones is as follows, where we prove that a number in said list will divide the product of the list. Isabelle/HOL: Very implicit; it's hard to tell what's going on, but the basic structure is there. Induct on the list, do some casing, apply a lemma about . Reasonably large. We have to destructure the membership quite manually, which gets a little troublesome. It's a fairly straightforward proof, though. Also not crazy, although it's hard to see the exact structure without comments (which I didn't write :P). This is a good time to point out HOL4 proofs are literally just SML terms! There's nothing more to it! The combinators and (for apply latter to all subgoals of former, and to one subgoal of former resp.) are just infix functions composing other functions! It's all just SML! You interact with HOL4 through a REPL, so you construct stuff dynamically, but then you have to puzzle piece your function together afterwards. Once you know that, it's more obvious what's going on; we induct, handle the first case, then simplification on give us two goals ( and resp.) Very explicit, but also quite concise. Matching on the list membership is quite intuitive, because the Agda mode in Emacs includes a command to automatically case split on basically everything. While it's much more implicit in Isabelle/HOL and HOL4 (a common theme), all four of these proofs take the form of asking whether the value we care about is at the head of the list, or somewhere later on, and that decides what we fill in divisibility with. Then, Primality! Isabelle/HOL: In Agda we also define what it means to be composite as a "positive" definition, instead of just "not prime"; this makes working with it quite a bit easier. The next "interesting" proof is proving that every not-prime number greater than one has a prime factor. In Agda this is part of the definition of being composite, so we don't bother including it. We're going to move slightly faster from now on, so I won't explain each snippet. Just compare yourselves. Isabelle/HOL: The steps of ~> and ~> in the HOL4 one annoyed me a lot, but I couldn't figure out how to golf them down. Similarly, this line: of the Lean proof causes me pain. We're almost there now! Two more steps to go: Prove there's always a prime outside a given set (list) of numbers, and use that to show the final statement. First, the former: Isabelle/HOL: The Agda proof differs slightly to accommodate the lack of ranges later. The Isabelle/HOL proof clearly wins in terms of length here, but it's also really unclear what's going on. Everyone else gets progressively more verbose, and the HOL4 proof in particular here is a bit nastily nested. (a first-order solver) does a lot of heavy lifting, as does . If you're wondering why both Isabelle/HOL and HOL4 have something named / , it's because it was ported to Isabelle/HOL from HOL4. We arrive at our final statement! Agda requires some more fiddling as it doesn't have ranges built in like the other two do, but we use our lemma above to construct the list , and then show there's a prime outside that (and that it hence must be above ). Isabelle/HOL: It annoys me I couldn't get this smaller, but oh well. We've done it! Euclid would be proud. (probably) It's now time for more opinions! I have five criteria I'll be ranking on: Not much to comment on here, really. is a great boon, and both Isabelle/HOL and HOL4's theorem discovery tools are great. Lean was reasonably close behind, with often giving good related lemmas as a solve, and Agda was clearly last. Paging through files online to find lemmas is annoying. Love it or hate it, Agda being entirely raw proof terms means things are essentially exactly what you tell them to be. There's never a moment where you're going "Damn, why won't the simplifier just expand this but not that!". Lean is pretty good here, as it's quite conservative around what it chooses to manipulate and everything is explicitly named. HOL4 has a pretty reasonable learning curve as one learns to use things like that can target based on patterns (e.g. ), but once you figure it out it's not bad. Isabelle/HOL really isn't stunning here; it's often hard to get it to do exactly what you want. I had a great time learning both HOL4 and Lean, but HOL4 edges out because it's such a unique interaction mode and it's still very powerful. Lean was fun, although annoying at some times, and Isabelle/HOL wasn't particularly interesting, but some of that is because i'm familiar with it. Agda sort of sucked at times; writing a whole primality decision procedure and fiddling with type nonsense got quite annoying after a while. Agda "wins" for the same reasons as above. Having to do really manual proof search and fiddling constantly wasn't super pleasant. HOL4 and Lean both had their own annoyances and I think it's unfair to rank one over the other; the learning curve on assumption manipulation / sim was quite significant in HOL4 and Lean's automated tools were finicky enough it quite sucked at times. Isabelle/HOL i'm just used to, so there's some bias there. Same reasons as above; there were a lot of times where HOL4 just had me going "huh????" because some theorem-tactic wasn't doing what I expected it to, or was transforming the goal in an unpredictable way. Lean had similar, where it would just randomly decide "erm actually i'm not going to solve this really simple goal for you with do it yourself please" in ways that left me baffled. Seriously, sometimes is smarter than and sometimes it's stupider than . Weird. Isabelle/HOL had some of the same but was generally fine, and Agda was utterly predictable. HOL4! I had a great time learning it, it's a seriously interesting system. I didn't not enjoy Lean, but there's enough odd stuff going on to make me slightly wary of it, I suppose. Isabelle/HOL remains the one I'm best at (I am somewhat paid to write it, so that helps), and Agda is Agda. What should you try? Well, all of them, but I would at least try out something new. If you've only used dependent theorem provers before, try Isabelle/HOL or HOL4, and vice versa. If you've only used theorem provers that work fully interactively like Lean, try HOL4 or Agda! New experiences are the joys of life. Isabelle/HOL: LCF-style: Isabelle/HOL, HOL4 Dependent-style: Lean, Agda High-interactivity: Isabelle/HOL, Lean Low-interactivity: HOL4, Agda High-automation: Isabelle/HOL, HOL4 Medium-automation: Lean Low-automation: Agda 0: 2 (instant) 1: 3 (instant) 2: 7 (instant) 3: 5 (instant) 4: 11 (quarter second) 5: 7 (quarter second) 7: 61 (10s) 8: 19 (40s) Aren't built in. Aren't as good. Isabelle/HOL: 117 LOC, with 19 proofs. Lean: 155 LOC, with 12 proofs. HOL4: 190 LOC, with 16 proofs. Agda: 264 LOC, with 45 proofs (29, not counting blocks) Ease of proof discovery (how easy is it to figure out what I want to do) Ease of proof manipulation (how easy is it to do what I want) Enjoyment (how much fun did I have) Annoyance factor (how often was I going "ugh!") Puzzled factor (how often did I go "why can't you solve this??") Isabelle/HOL Isabelle/HOL Isabelle/HOL HOL4 / Lean (tied second) Isabelle/HOL Isabelle/HOL

0 views
Jeff Geerling Yesterday

Radxa's Q8B has 2x the performance and expansion of the Pi 5

There was a time I'd look at a board like the Radxa Dragon Q8B (at left, above) and be like, "there's no way I'd spend $209 on an SBC with 8 gigs of RAM". But we're in 2026, and seeing the 8 gig Raspberry Pi 5 going for almost the same amount, I figured I'd give it a shot. On paper , the Q8B beats the Pi 5 in pretty much every way. A lot of that is thanks to this Snapdragon 8cx Gen 3 chip, which is the same chip I tested on Microsoft's Windows Dev Kit 2023 .

0 views
Chris Coyier Yesterday

Justice for CSS

Fun seeing CSS be a topic in WIRED . Pete Millspaugh shouting out some greats: One programmer recently re-created Doom in CSS . Others have used it to build holographic Pokémon cards and 3D-rendering engines . Cassidy Williams, who competed in this year’s inaugural March MadCSS tournament , built an experimental database-query engine entirely in CSS. I mean, hell yeah. Allow me to just… And I think Adam did it first!

0 views
Kev Quirk Yesterday

2026-10-09 20:15: First fire of the year and Sid is loving it. Not sure we appreciated the...

First fire of the year and Sid is loving it. Not sure we appreciated the giant queen wasp that came bumbling out of the chimney though. Thanks for reading this post via RSS. RSS is ace, and so are you. ❤️ You can reply to this post by email , or leave a comment .

0 views
Unsung Yesterday

Subtitles on demand

Nice moment in iOS: when you reduce the volume to zero, subtitles come up automatically – and they go away the moment you increase the volume again. This is from YouTube on the iPad, but it appears to be system-wide: (Feels extra meaningful in the face of so many people playing their media on speaker in public these days.)

0 views
Stratechery Yesterday

2026.41: It’s Not You, It’s Me

Welcome back to This Week in Stratechery! As a reminder, each week, every Friday, we’re sending out this overview of content in the Stratechery bundle; highlighted links are free for everyone . Additionally, you have complete control over what we send to you. If you don’t want to receive This Week in Stratechery emails (there is no podcast), please uncheck the box in your delivery settings . On that note, here were a few of our favorites this week. This week’s Stratechery video is on Apps, Agents, and Aggregation . Drifting Apart . For the last 25 years, Apple has been in a position where its computers were not only thought of as the best choice for everyday consumers, but also the most useful tools for technologists and hackers. However, I think those paths are diverging: in Apple and a Hacker’s Future I explain why I feel myself growing increasingly frustrated with Apple in the age of AI; that means that Apple partnering with LG to dramatically expand its home offering is not for me, which paradoxically means it’s a great idea. The future of consumer technology is likely completely custom on one hand, and completely integrated on the other. — Ben Thompson It’s Complicated. As someone who was born in D.C. and therefore takes an interest in politics as a birthright (or birth defect), I loved this week’s Stratechery Interview with author and political consultant Katie Harbath. Ben and Katie trace the early innings of tech’s impact on politics, including several flashpoints I’d forgotten (John Kerry and dolphins!), but then turn to ten years of Katie’s experience at Facebook. Her tenure coincided with seismic political shifts and subsequent sentiment shifts toward tech companies, and both Ben and Katie — who’ve been friends for 20 years — reflect on that era with an honest and fun look at evolving business imperatives, angry backlashes, and the explanatory power (or lack thereof) of tech as a political force. — Andrew Sharp Friends Without Benefits.  Speaking of politics… Sharp China was off this week, but two weeks after Xi Jinping’s visit to D.C., I wrote about the delightful absurdity of U.S.-China dynamics in the current moment , and the quiet effectiveness of his administration’s campaigns to counter Beijing. One year after I wrote that China threatening to cut off the Western world from rare earths would do lasting damage to its global standing, Germany and France are now lobbying for new trade barriers and a “China kill switch” that could shut off Chinese imports entirely. Trump, meanwhile, is friendlier than ever with Xi, as the U.S. attempts to preserve stability while its policies complicate Beijing’s relationships everywhere else.  — AS Apple and a Hacker’s Future — I was happy for years in Apple’s walled garden; with AI, however, their protections feel like limitations. Game Decompilation, Is This Legal?, A Well-Trodden Path — Games are being decompiled, but the real risk to gaming is new games and increased personalization. Apple and LG, The House For Everyone Else, Agent Standards and Amazon — Apple is taking a smarter approach to the home than I expected, leaning into integration (with partners); then, what Amazon should do about agents. An Interview with Katie Harbath About Disrupting Politics at Facebook — An interview with former Facebook Head of Global Elections Katie Harbath about her new book Disrupting Politics, and how things change for the company in the 2010s. Friends Without Benefits — The Trump methods are often maddening, but the current administration’s strategy on China continues to be quietly effective. Ben Gets Hacked Apple’s 2010s Mistakes The Fall of Brazil’s Armored Vehicle King TSMC is Coming to Texas? Fraud Watch 2026, Sixth Men and 32 Teams and KAT, All Eyes on the Heat and the Southeast Two Paths for Apple and Its Users, More on Amazon and Advertising, OpenAI and 722 Mathematical Manuscripts

0 views
Giles's blog Yesterday

Fun with low-rank vocab matrices (and a bonus test loss reduction?)

I was nerdsniped ! On the HF discussion page for one of the models I created for my previous post , asked if I'd considered trying out factorised embeddings -- something he's using for his model, Maba, and which was previously used in some other models, like ALBERT . It's a really nifty idea; you use a similar trick to LoRA as a way of reducing the number of parameters used for your embeddings and your output head. And for small models, those can be a disproportionate number of the total. For example, with my 163 million parameter GPT-2 small-style models, the embeddings are about 39 million of them ; the output head is the same size, so with those two taken together, that's half the model just getting stuff in and out rather than actually doing the thinking. Even if you use weight tying, like the original GPT-2 models did, you'll wind up spending 30% of your "budget" on the single matrix shared between embeddings and the output head. Similarly, while larger models have a smaller percentage spent that way, even medium-sized MoE models can wind up spending a lot of the active parameters on embeddings; I calculated that for Qwen 3.6 35B MoE, with 3B active parameters, there were about 1B of them used across both the input embeddings and the output head. So anything that can reduce that -- so long as it doesn't come at a high cost in terms of the model's capabilities -- is worth considering. You save on your parameter count, which either means smaller models and potentially quicker training, or allows you to "invest" the savings in more thinking parameters -- that is, a wider network with a higher embedding dimensionality, or a deeper one with more layers. Andrew reported that the impact of using this trick was minimal: At rank 128 on a 50k vocabulary, the penalty on validation cross-entropy is negligible (typically within +0.02 to +0.04 loss, or <0.5 perplexity delta). Now, that suggests that he's getting a loss of around 2.5 (that being the point where a loss increase of 0.04 implies a perplexity change of 0.5), which is much lower than I typically get with my GPT-2 architecture (3.5 is more like it for me), but still, perhaps I'd get good numbers too? I decided to train a few models to see what happened. The results were interesting! I found that using this trick on both the embeddings and the output head caused a somewhat larger increase in loss than Andrew described -- about 0.07 in my first test, 0.10 in the second, and 0.14 in the third. Those are relatively large, though potentially recoverable from further training or larger models. But more surprisingly, I found that using the trick on the input embeddings only seemed to reduce test loss. Before I'd started, I'd expected it to be less harmful on the input side than it was on the output side, but seeing an improvement was certainly unexpected. Getting loss down by reducing your number of parameters is not what normally happens! So, it's definitely worth digging in a bit. Let's start with the theory: what are these factorised embeddings, and how do they work? Like LoRA, they rely on low-rank factors, so firstly I'll define those. Our models are made up of a large set of matrices -- embeddings, output heads, attention weights, FFN linear layers, and so on. Making them smaller obviously reduces the number of parameters for the model, though you would expect it to come at a cost. The idea behind low-rank factors is that you can replace a larger matrix with two smaller ones that will contain most of the important information. Imagine that you've got a matrix of size m × n . Now, from matrix multiplication, we know that if you multiply an m × r matrix by an r × n one, you'll get a result that is m × n . If we do that, then we've factorised the matrix (in the same way as we might factorise 12 into 3 and 4 because 3 × 4 = 12 ), and the value r is referred to (logically enough) as the rank of the factorisation. If r is sufficiently smaller than m and n , then these two matrices -- the low-rank factors -- combined will contain fewer parameters than the full matrix. Let's make this specific, using the output head of a GPT-2 style model without weight tying. It takes in the embeddings that result from the Transformer layers (after normalisation), and converts them into logits across the vocabulary. For the GPT-2 small size, our embeddings are 768-dimensional, and the vocab size is 50,257 tokens. So when we use a linear layer to do that mapping, it has 768 × 50257 = 38597376 parameters. If we were to replace it with two matrices -- say, one of 768 × 128 and one of 128 × 50257 , then combined they would take up 768 × 128 + 50257 × 128 = 98304 + 6432896 = 6531200 parameters. That is almost six times smaller! So: the idea is that instead of creating our model with an m × n matrix, we create it with a pair, m × r and r × n , and train those instead. If all goes well, that pair will be almost as capable of learning what we want as the full one would have been, so we'll get results that are close enough. The maths and the implementation work out simply, too. For a linear layer with no bias, we can write the matrix multiplication that takes our inputs X and a weight matrix W , and produces an output Z , like this: 1 Now, if we're using a pair of low-rank factor matrices A and B instead of a full one, W , we can say the "virtual" weights we want to use for the calculation are W ′ such that: So that means that our calculation for this neural network is this: Matrix multiplication is associative, which means that you can rewrite that as: ...which hopefully you can see is the same as feeding X through a layer using A as its weights, and then feeding the result through a second one using B . In code, you've taken something like this: ...and replaced it with this: It's probably intuitively obvious, though, that this comes at a cost. If you have fewer parameters then you can store less information, so this part of your model is "dumber". If it's not clear, though, imagine that in the code above was one. You would be taking the (for GPT-2 small) 768-dimensional embedding, converting it to a single number, and then expanding that single number out to a 50,257-dimensional set of logits. Stuff is going to get lost -- the idea behind low-rank factors is that, so long as you choose an appropriate value for r (which is often referred to as the width of the low-rank bottleneck ), you won't lose the important stuff. This works surprisingly well in many cases -- in particular, LoRA, which allows you to fine-tune models that are too hard to fully train on your hardware, or to fine-tune them faster, uses it to easily train something like low rank factor "diffs" to your weight matrices 2 . But for this post, we'll try the simplest version: what if we replace both the input embeddings and the output head -- the vocabulary matrices -- in their entirety with low-rank bottlenecks? Low-rank factorisation of the vocabulary matrices is a bit of a mouthful, so based on the name "LoRA", I decided to call this trick LoRE, for low-rank embeddings. It's not strictly accurate (after all, we're doing it both to the embedding matrix at the start of the LLM and to the output head at the end), and I don't expect it to take off, but I rather like it and will use it in this post :-) The argument behind it is that the embeddings are just a simple lookup table, so are exactly the kind of place you'd expect to be able to make savings by only considering the important parts of our huge matrix; the same might apply to the output head at the end, though personally I was less convinced by this part. It's worth looking into that asymmetry a bit. My intuition was that while embeddings really are a lookup table, the output head is doing something a bit more subtle. It's projecting from the continuous embeddings that come out of our Transformer layers into logits, which we interpret (via softmax) as a probability distribution over possible next tokens. That's a significantly less simple job than mapping from "cat" to the appropriate embedding: as a (simplified) example, if you have an embedding that means something adjacent to "cat", "dog", "gerbil", "household pet" and so on, then projecting that to the appropriate values for the next token is non-trivial. 3 Still, implementation-wise, it was really simple. I decided to extend the PyTorch code that I had from Sebastian Raschka 's book " Build a Large Language Model (from Scratch) ", by adding an optional section to the model config JSON. This would allow us to switch on LoRE mode for the input embeddings and the output head independently, and would specify the rank -- that is, the r in the section above, which says how wide the low-rank bottleneck between matrices A and B would be. So, in code, my first cut changed this: ...to this: ...and this: ...became this: That in itself was a perfectly reasonable implementation of the underlying concept. But it had a problem. I wanted to compare the loss with and without LoRE, and also find out what the effects of input embedding-only and output-head-only LoRE would be. But I've found in other experiments that the initial random weights that my models start with can have a significant effect on the loss that the resulting model gets. The code above would give quite different random weights with different configurations. The fix was simple, though: With that code, so long as there is any LoRE config, we create the same weights regardless of whether it's used in the input embeddings or the output head. I would need to train a baseline which had config for LoRE but just had both and set to there -- that would actually be a normal, non-LoRE model but would have the same initial random weights in any parts that it shared with an equivalent model that did use LoRE. Additionally, Andrew had said that we need to be careful about initialisation: The main failure mode to watch for during training is early gradient spikes: scaling the bottleneck projection initialization to 1 / sqrt(r) keeps variance uniform and ensures training dynamics match the full-rank baseline from step 1. ...and later : Keep standard GPT-2 init on the embedding table, but scale the inner linear projection matrices by std = 1.0 / math.sqrt(128). (The 128 in there is because we were talking about a setup with r = 128 , which is actually what I wound up using.) Now, I was using PyTorch's default initialisation rather than the classic GPT-2 setup, but I went ahead and added a flag to handle the scaling as Andrew described: if it was set, then right at the end of the model creation I applied the initialisation to the low rank factor matrices that were innermost in my model (as in, closest to the Transformer layers): Even though that was not run for every configuration, because it happened right at the end of the model creation, it would not affect the other weights, so I figured that it would be safe. You can see the full diff from the normal GPT-2 code here . Those changes looked correct to me, and I asked GPT-6 Astra (on "extra high" thinking) to confirm that it looked right to it in the context of the discussion, which it did. That done, I double-checked with Andrew , as I really wanted this to be a clean attempt at a repro of his results. He confirmed, so it was time to train some models! I decided that I wanted five training runs to check this out thoroughly: To save time, I decided to train them in the cloud: the first three, and then the last two, in two batches of parallel runs. I used 8x A100 machines with 40 GiB VRAM per GPU on Lambda . I'll break with my normal tradition of giving detailed runthroughs of each training run, as there are (spoiler) quite a lot of them in this post! However, for reproducibility, the commands I ran for each one looked like this: ...with the run ID, , replaced with the appropriate one for the given run settings . Here are the results from the first three runs: the baseline, and the ones with LoRE at both ends, with and without smart initialisation. The model name links go to the uploaded models on Hugging Face. You can see that I had some issues with the last run; there were shortages of available instances, and I wound up starting one in Japan. Connectivity to it from my home in Portugal was really slow and unreliable; when I tried to download the model after the training run, was predicting 10 hours (which at the machine's cost of US$15.92/hour would have been insane). However, I was able to copy it to my PythonAnywhere account quickly, perhaps because that is in a US Amazon datacenter and had better connectivity to Japan, and then I could copy it from there to my machine, again quite quickly. Unfortunately while scrabbling around with that I didn't capture all of the output. Still, the important data at this stage was in the test loss column. As expected, using LoRE made the test loss worse. And smart initialisation did seem to help reduce that penalty. The loss delta, at +0.07, was worse than the +0.02 to +0.04 that Andrew described in his message, but not wildly different -- certainly small enough that it seemed plausible that you could recover it, and perhaps more, by investing the 64M parameter difference in a deeper or wider model. Promising! The cost and time savings were real, too: the run in Japan had its cost bumped up by all of the woes I had copying the model down, so the one is the best indication: US$38.55 rather than US$43.96, so a saving of more than 10%. And while going down from a bit more than 2h30m to 2h14m might not seem like much, with a larger model or a longer training run, an almost 14% reduction could be valuable in and of itself. (And that's not even considering the alternative of "reinvesting" the saved parameters in larger models.) So that was pretty good news! It was time to do the ablation runs to see whether having LoRE just on the token embeddings, or just on the output head, made things any different. I switched the setting for the remaining two models to , and kicked them off. Now, there's a bunch of interesting stuff in there, but let's focus on the test loss. My lab notes for this bit say "well, that's a bit of a shocker!" Quite amazingly -- at least to me -- we got lower test loss with the input-only LoRE, with 3.526610, than we did with the no-LoRE baseline, which got 3.599611. Things get even more interesting when you compare the different versions (excluding the non-smart-init) against each other, in terms of their difference from the no-LoRE baseline (which I'll call the delta for conciseness below). Rounding to 3dps: If you add the two single-LoRE loss deltas together -- the 0.138 and the -0.073 -- you get 0.065, which is surprisingly close to the delta of 0.072 for the dual-LoRE option, just 0.007 away. Could we be looking at two almost independent effects, one for each option of where to apply the LoRE? And was that apparent benefit of the input-only LoRE a real thing? Or was it due to chance -- perhaps we had "good luck" when initialising the LoRE weights, and "bad luck" when initialising the non-LoRE ones. If there was an overlap between the best loss you could get with LoRE and the worst loss you could get without, then this result could be within the noise. I decided I was going to do a second batch of training runs to see if I could get evidence one way or the other. But before we get into that, it's worth taking a look at some of the other numbers in those two tables. Firstly, let's take a look at the training time. The training machines looked like they were running at close to 100% during all of the runs, so tentatively let's assume that time taken is proportional to compute. Unsurprisingly, the baseline run came in with the longest time, at 9,339s. And equally unsurprisingly, the full-LoRE run that we have timing for was much faster, at 8,057s. It certainly makes sense that replacing big matrices with pairs of (much) smaller low-rank factors will mean fewer calculations on both the forward and the backward pass, meaning that the training run is faster. There was something that initially surprised me with the single-LoRE runs. Using LoRE on the output head sped things up quite a lot, but input embedding LoRE had much less effect. However, after thinking about it a bit, it became clear what was going on. An embedding module in a network is actually really quick to run, both on the forward and backward pass. While I like to think of embeddings as conceptually being a projection of a one-hot vector in vocab space into embedding space via a matrix multiplication, and I still think that's an excellent model of interpreting what's going on, in practice it's just something much more like an array lookup, with almost zero cost. Likewise on the backward pass, we only need to work out gradients for the chosen embedding, so that should be faster too. Indeed, with that all in mind, it might not have been surprising if input-only LoRE had turned out to be a bit slower than the baseline, as it, at least, needed to do forward and backward passes through actual matrices, even though they were fairly small. Doing another of those delta tables, the time difference in seconds (using the "ordinary init" run for the both-on number): You can see that if you add the delta of the single-LoRE options, you get -1,251, which is pleasingly close to the delta of the dual-LoRE one. And that is much less surprising than the loss result -- with training compute, you really would expect improvements like this to be additive. Finally, there was something interesting in the initial training loss. Because my training code prints out the loss it got on the first global step, I decided to note it down. There's something in this data that will become important later: in both of the training runs with LoRE on the output head and smart initialisation, it went up noticeably. Normally, the initial training loss on my GPT-2-style models is a bit less than 11. This fits in well with the architecture; you'd expect that a model that was predicting tokens purely randomly (well, strictly, uniformly) would have a perplexity roughly equal to the vocab size; the vocab size for the GPT-2 tokeniser is 50,257, and loss is the natural logarithm of perplexity, so that implies a loss of roughly 10.82. But both of those smart-init models with LoRE on the output head had an initial loss about one point higher, at 11.865 and 11.817, meaning that they were significantly worse than random. What might be going on here? We'll find out later :-) Anyway, for now, that was an interesting set of results. I wanted to dig in more; in particular, would that surprising improvement of test loss for the input-only LoRE model reproduce if I tried again with a different random seed? I had two working hypotheses at this point; either A solid and simple test to try to distinguish between these was just to train another set of models, with a different random seed. If I got the same kind of results, input LoRE beating non-LoRE, that would be evidence in favour of (2) rather than (1), whereas if things changed, it would work the other way. I decided not to bother with a non-smart-init model this time, so I set things up for four new models. My training code uses a random seed of 42 by default, but allows it to be overridden in the config file, so I decided to use 123 for these, and created: Once I had the config together, it was time to train the models -- but it was hard to get available instances on Lambda. I wound up having to use my script to start things up, but after a few hours I got an alert on my phone that I had instances running, and could kick things off. The second training run with input-only LoRE came in with a test loss that once again beat the baseline, so I did the full set of runs, and here are the results: Another matrix of deltas against the baseline: So, once again, input-only LoRE improved test loss (though at -0.013, it was a smaller effect than the -0.073 the previous set of models had). And once again, the sum of the input-only and output-only LoRE deltas was close to the combined-LoRE model's -- indeed it was even closer, 0.102 being just 0.001 away from 0.101. The training time results and the higher initial training loss for models with LoRE on the output head also held up, which was good to see. So at this point it was time to wrap things up -- or was it? While I was doing the second batch of training runs, I started writing up this experiment. As I normally do , I ran a draft past various AI models, and Claude Opus 5.5 on max thinking spotted something. Andrew had written : Keep standard GPT-2 init on the embedding table, but scale the inner linear projection matrices by std = 1.0 / math.sqrt(128). I'd interpreted that "inner" as meaning that the "innermost" matrices in our low rank factors -- the ones that were closest to the Transformer layers -- should be initialised as he said, with values drawn from a normal distribution with a standard deviation of 1 / r , and a mean of zero. So that implied the second matrix in the embeddings, and the first one in the output head: Claude felt that it should be the second low-rank factor in both cases -- that is, we should change It made a very good case for doing things that way, and digging into that is useful because it changes this "smart" initialisation from being a blindly-implemented "secret sauce" into something actually meaningful. Let's imagine that we're not using LoRE, and consider the output head only. It is a PyTorch , which means that: ...the values are initialized from 𝒰 ( − k , k ) , where k = 1 in_features So, we have a matrix, which we can call W , that is full of numbers drawn from that probability distribution -- a uniform (flat) distribution within the range from − k to k . For LoRE, we're replacing W with two separate matrices, which we'll call A and B : Let's say that W is shaped m × n , which means that A is m × r , and B is r × n . We want the combined effect of those two matrices W ′ = A B to start off with random numbers that look like -- in terms of their randomness -- the full matrix W . But what do the numbers actually look like in our "virtual" matrix W ′ with the code above? On the face of it, it sounds unlikely to be anything like the probability distribution for W . After all, W was initialised based on a formula that used in_features . You can see that A will have been initialised using the same distribution, as it has the same number of input features, but the number of input features for B is r , so its random numbers will have been based on that instead. Their combination into W ′ will presumably blend something from each of those two different probability distributions. We can actually work out what that will be. Maths incoming: click here to skip . Per Wikipedia , the variance of the product of two independent random scalar variables (so, not matrices, but we'll come back to that) X and Y is this: ...where σ X 2 is X 's variance, μ X is its mean, and likewise for Y . Now, let's say that the mean is zero for both X and Y (like it is for PyTorch's distribution for the initial weights, 𝒰 ( − k , k ) ). That simplifies the above: How does that apply to our matrices? Well, let's write out how we calculate W ′ by multiplying A and B , assuming that m = 3 , n = 4 , and r = 2 : By normal matrix maths, the value at position 0 , 0 in the result will be the dot product of the zeroth row in the first matrix (taken as a vector) and the zeroth column in the second: We can rewrite that for an arbitrary low rank bottleneck r like this: ...and even more generally, we can define all of the items in W ′ like this: So, every element is the sum of r products, where each product multiplies a number from whatever distribution was used to initialise A 's elements by a number from whatever was used for B 's. Using the notation from above, A 's elements have variance σ A 2 and B 's have variance σ B 2 . So that means that the variance of each component of that sum is σ A 2 · σ B 2 . There are r of them; if you add together independent variables, their variances add, so that means that the variance of the elements of our resulting W ′ is: Now, let's remember that our matrix A actually already was initialised in the way we would have liked our non-LoRE version W to have been done. The distribution of the random initial weights for an is dependent entirely on the number of input features -- and of course A has the same number of input features as W . So how can we make Var ( W ′ ) be σ A 2 ? We need to make σ B 2 = 1 / r , and then the equation above drops out like this: Now, let's look at the code (with Claude's correction in there): We're setting the weights on our B matrix to be drawn from a distribution with a standard deviation of 1 / r . SD is, of course, the square root of the variance (which is why we've been using things like σ B 2 with that squaring in there to represent variance -- σ on its own is used for standard deviation). So the variance of the matrix after we've called that on it will be 1 / r as desired, and W ′ will have random initial weights with the same variance as W would have done if we'd created it directly. That's rather satisfying :-) So that's the output head. How about the input embeddings? They're s, which are initialised somewhat differently: initialized from 𝒩 ( 0 , 1 ) That's a normal distribution, with a mean of 0 and a variance (and thus also a standard deviation) of 1. The maths above applied to any distribution with a mean of zero -- so the smart initialisation should work for those too. Our A matrix would have the correct variance, 1, and a mean of zero, and therefore so would A B , given that (for embeddings) B already had the smart initialisation. So does that mean that our W ′ "virtual" matrix created by multiplying A and B is identical in terms of randomness to the matrix W that it's replacing? Well, not quite. Remember that the output head had numbers drawn from a uniform distribution, and the embeddings from a normal distribution. We're multiplying the A matrices that are the "input" low rank factor matrices by B s that are initialised from a normal distribution. The variance of the A matrices is maintained by the smart initialisation, as we've shown, and the mean (being zero) is going to come through cleanly too. But the shape will change. I did a bit of digging around and it started to feel like a bit of a rabbit hole, but the one thing I was able to be certain of is that a variable drawn from a uniform distribution multiplied by another from a normal distribution gives a result that is neither uniform nor normal, and that normal times normal gives something called a normal product distribution (or also a product-normal distribution), which is also neither uniform nor normal. Remember that each element of our W ′ matrix is defined by this: So each one is a sum of r numbers, each of which is drawn from a product normal distribution (for embeddings) or from whatever the uniform × normal distribution is called. What shape would that be? Again: rabbit hole, but the central limit theorem states ( per Wolfram MathWorld ): the normalized sum of independent random variates with finite variances approaches a normal distribution So, for large r , we can say that the result is going to be close to a normal distribution. 4 What the smart initialisation does is make sure that our "virtual" weights, W ′ = A B , have the same mean and variance as the ones we're trying to approximate, W . But it won't keep the same shape for the distribution that they're drawn from -- certainly not for the output head, which goes from uniform to normal-ish. The embeddings are less impacted (though not completely untouched) because they were normal and are still almost so. Still, it's a neat trick! Was it what Andrew had actually meant? Having convinced myself that the smart initialisation code I'd been using was wrong, I decided to check with Andrew. My first thought was that perhaps he was using weight tying -- remember, with weight tying, the embedding matrix is just re-used in transposed form for the output head. That would mean that the embeddings would be W ′ = A B , and you'd use the smart initialisation on B , but the output head -- being that transpose -- would use W ′ T = B T A T for the same B and A , so the smart initialisation would be the other way around. But as it turned out, it was just a miscommunication . He said that he keeps his weights untied, and had been using the word "inner" in "inner linear projection matrices" to mean something different to what I'd interpreted it as. He confirmed that the real smart init code should always be applied to the second matrix, as the maths (and Claude) suggested. So that was a simple change. You can see the diff here , but in short: Now, the good news (both for my own sanity and my wallet) was that testing this fix was not going to require another four training runs. My training code is essentially deterministic -- no dropout or any other randomness is used after the model is created 5 . Because the smart initialisation code was at the end of the model creation, and smart initialisation of the output head was right at the end, that meant that changing it would not affect any other code that used randomness. So if I did two training runs -- with LoRE switched on for the output head only, and with it switched on for both embeddings and output -- then those would be "compatible" with earlier training runs that had no LoRE at all, and that only had it on the embeddings. You can see the configs here (with no explicit random seed, so they'd use my default of 42): Here are the results; I've put them into a table with their counterparts from the original seed-42 training run: Before we look at the test loss, check out that "Initial training loss" column. The weirdness that I'd noticed earlier, where that value was much worse than uniform, is gone! That actually makes some kind of sense. With the smart initialisation on the wrong part of the low-rank output head, our variance was completely wrong, and so the model was initially producing particularly bad results. 6 So that was promising! But the test loss results were even more interesting. In our original seed-42 results with the incorrect init, the output-head-LoRE-only model got a test loss of 3.737128, but here we got 3.785209. It was actually worse with the corrected smart initialisation! And that carried through to the result for models with LoRE on both input and output; the original model with the incorrect init got 3.671585, and here we got 3.741209 -- an even bigger worsening. Combining those two together, an image I like in terms of the loss landscape is that previously we were starting on a mountain that was near a deep valley -- we started with high loss, but there was a low-loss place nearby. But with the smart initialisation fixed, we were now starting on a hill with a less-deep valley nearby. So what happens if we do one of our test loss delta tables showing how each model performed against the baseline? If we add up the effect of the input-only test loss delta of -0.073 and the output-only delta of 0.186, we get 0.113 -- quite different to the delta of 0.142 that we actually got with them both. That nice "additive" property that we had, where the delta from input LoRE only plus the delta from output LoRE only summed to almost exactly the same as the delta for LoRE on both ends, appears to have gone away :-( Still, an interesting set of results! Let's bring everything together. Here are all of the training runs together in one table. I've removed the columns for the cost, the end training loss, and the training time to keep things manageable, and I've sorted it by the test loss. A few things stand out: So what does that all tell us? The numbers above suggest three things -- with important caveats below: Even more caveated, we might say: Neither the larger of the two apparent improvements from input-only LoRE nor the worsening from output-only were small -- when I was trying various interventions into my GPT-2 models (like removing dropout, scheduling the learning rate, gradient clipping and so on), many of them had a similar or smaller level of effect. Similarly, training a comparable non-LoRE model on double the number of Chinchilla-optimal tokens (ie. on 40 per parameter rather than 20) improved loss by 0.09, while investing the same compute resources to do a Chinchilla-optimal training run on a larger model improved it by roughly 0.13 over the baseline (see this post for the raw numbers). So, is input-only LoRE One Weird Trick To Improve Your Test Loss? Of course not. Are output-only LoRE and both-ends LoRE Bad Things? Not necessarily. The first thing to remember is that this is a really limited set of experiments. Although I wound up spending about US$450 on training runs (I really should be investing in building my machine up as a better training box to save on Lambda costs), I was only able to test: Even in order to say anything definitive about whether LoRE works for this specific architecture, it would be necessary to do tests over a much larger number of random seeds and different lengths (in terms of number of tokens) of training run: To get solid results on whether smart initialisation is a good thing, you'd need to try a number of seeds to see whether the poor performance of the "correct" smart initialisation against the "incorrect" one worked out as a general result. And if it did, why might that be? Beyond that: the apparent improvement in the loss from input-only LoRE is something that came up in these experiments. Maybe it would turn out to be a real thing, maybe not, but the real benefit that Andrew mentioned in his original message was about something quite different: LoRE saves a lot of parameters and only (as he said later) costs a small amount of loss. If you reinvest those saved parameters in a deeper network with more layers, you can hopefully gain back the loss that you, um, lost, and then some -- and wind up with a more capable model. So important further tests (which I think I will do, but later on) would be: It's worth noting that in my Chinchilla experiments, I scaled up the model by 2 . That's about a 41% increase, which is quite close to the 39% we save by using LoRE on both ends. So if the loss improvements carried over, perhaps it might work? On the other hand, those models were also trained on 41% more tokens, so... So there's a huge number of further experiments that would be needed to build out these results -- and that's even before we move beyond this specific architecture. Andrew reports solid results with his setup, and his model Maba does appear to be quite different. But would it extend to a Qwen-style one? Or Mistral? Next, there's what happens with scaling. LoRE is valuable in small models because embeddings and the output head are such a large proportion of the total parameter count. My guess is that it would become increasingly unhelpful as models got larger. To take an extreme case, looking at the Kimi K3 paper , it has a vocab size of 160k, and its hidden dimension (which I'll assume is what the embeddings are using) is 7,168. That means that the embedding layer uses something like 1,146,880,000 parameters, as does the output head, for a total of ~2.3B parameters (assuming they're not using weight tying, which seems likely for a monster like this). It has 104.2B active parameters per token, so if it were to use LoRE you'd save something of the order of 2% of the active parameter count. But for purposes of "reinvesting" in further layers, the real comparison point is the total number of parameters, not the active ones, and with about 2.8T total, the number used for embeddings is less than 0.1%. It doesn't sound like it would help much. Unless, of course, the benefit of the input-only LoRE loss improvement actually turned out to be a real thing, and didn't weaken as the model was scaled... But anyway, that's speculation. I think a good set of experiments for that would be to try the same training runs as before, but for larger models. Maybe just trying GPT-2 medium and large sizes would be a good start? Lots of work. If I had access to Google's resources then I think I'd be kicking off a bunch of training runs. OTOH if I had access to Google's resources I probably wouldn't be blogging about this... I think that there's one thing I'm going to take away from this. LoRE is an interesting intervention -- and I think is well worth trying out on any new model where vocab matrices are a significant fraction of the parameters, just to see if it helps. I'll be doing that in future. And if anyone else out there wants to try LoRE-style training runs, I'd love to hear from you. Any results, positive or negative, would be really interesting. Thanks for reading! And many, many thanks to Andrew for suggesting this as an idea to play around with -- it's been fun :-) This is often written Z = X W T to reflect the fact that weights are generally kept in d out × d in format, at least in PyTorch, but that's really an implementation detail .  ↩ I'll write more about LoRA in the future -- I've been playing with it a bit -- but essentially, what you do is: For each matrix that you want to train (which might not be all of them -- for fine-tuning, people often only train a subset), you add on a low-rank adapter , which is a pair of matrices like our A and B above, and which sits "beside" the existing one, like this: Gradient tracking is enabled on the matrices in the low-rank adapter, and its results are added to the results of the original weights. The idea is that the adapter pair learns to create a "diff" to the results of the original weights, which allows a certain amount of training of that part of your model. And it works surprisingly well. Again: I'll write about this in more depth in the future.  ↩ When I was discussing this with an LLM -- sadly I've forgotten which -- the softmax bottleneck came up here, as it did in later correspondence with Andrew. That's a reference to this paper . I'll need to work through it carefully at some later point, but the relevant point appears to be that the rank (which we can loosely read as how many independent ways the predictions can vary from one context to another) of the values coming out of softmax is limited by the rank of what is going into it. If we force our (in my GPT-2 small case) 768-dimensional embeddings through a 128-dimensional bottleneck, we're reducing their inherent rank, and it's that reduced rank that will drive softmax's, so the results will be worse than what you'd get with the original 768. Seems logical enough. Linkrot-proof reference: Yang, Z., Dai, Z., Salakhutdinov, R., & Cohen, W. W. (2018). Breaking the softmax bottleneck: A high-rank RNN language model. In International Conference on Learning Representations (ICLR) .  ↩ Thanks to Claude Opus 5.5 for pointing me at the central limit theorem. I definitely need to brush up on my statistics, and I'm sure I knew about it at some point back in the 90s...  ↩ Modulo CUDA jitter of various flavours -- though even then, a while back I did two training runs on 8x A100 machines with the same config, months apart, and the Safetensors files were identical bit-for-bit. So I think the effect of that in my setup is minuscule.  ↩ The temptation to dig into the details of why, and exactly what the mistaken smart initialisation did to the variance of the "virtual" weights W ′ , is strong. But I will resist.  ↩ When I ran a draft of this post past my editorial board of LLMs , Grok made the point that perhaps the apparent benefit of having LoRE only on the input embeddings might have been due to that model seeing significantly more tokens per parameter. It's an interesting thought! If we do the maths, the input-only and output-only LoRE models were trained on ~25 tokens per parameter and the both-ends ones were trained on about 33, vs 20 for the non-LoRE ones. However, in my Chinchilla experiments, I only got 0.09 improvement in loss by training on 40 tokens per parameter rather than 20. Now, I'm sure that gain mostly happened early in the run -- overtraining is subject to diminishing returns -- but the result of 0.073 for input-only LoRE would imply that almost all of it happened in the first extra 5 tokens per parameter, which seems dubious. Those are different training runs with different seeds, and were using my JAX code, which has a better baseline loss than my PyTorch code, so we can't compare them directly. But it feels unlikely that the effect would be drastically different. Also, if we use reductio ad absurdum on Grok's logic, it does sound a bit weak -- if we get rid of parameters but train on the same number of tokens, the higher tokens per parameter will not in general counteract the damage from the smaller model. Imagine, for example, removing 32M parameters worth of Transformer layers and training on the Chinchilla-optimal tokens for the size of the model before you did that. I'm not going to run the experiment, but I'd be... somewhat more than surprised if it improved the model.  ↩ A baseline. As I said earlier, the LoRE stuff would have an effect on the randomness used for the initial weights, so I wanted to train one model with LoRE "enabled" but not actually used. Config: , . A model trained with LoRE enabled on both the input embeddings and the output head, but without the smart initialisation of the low-rank matrices. This was simply to confirm to myself that it was required. Config: , . A model with LoRE on both ends, with the smart initialisation -- essentially, what Andrew had described. Config: , . A model with LoRE on the input embeddings only, using smart initialisation if that had turned out to be necessary, and not using it if it had not. I deliberately made the config invalid, using instead of or for the flag, so that I'd be reminded to fill those in later. Config: , . A model with LoRE on the output head only, with smart initialisation the same as with (4). Config: , . What we were seeing was due to luck of the draw with the random initialisation of the weights -- good luck with LoRE, bad luck without. There really was an effect here: input-only LoRE actually improved test loss in the resulting model. A new baseline with no LoRE. Config: , . An input-only LoRE. I wanted to run this one as the first non-baseline one, because if it got worse (higher) loss than the baseline, then it would look rather like the effect I'd previously seen was due to random weight initialisation, so I might want to consider stopping there. Config: , . If I decided to continue, the next one would be LoRE on both the input and output sides. Config: , . Finally, I'd do an output head LoRE only one. Config: , . I changed the config parameter so that instead of just being or , it could be , for the original incorrect interpretation, or for the fixed one. I updated all of the existing training configurations that had set to to be . I added on yet more config for some more training runs to test this, setting to the new option. Both: , . Output-only: , . The input-only LoRE models lead the pack -- though it's a close-run thing, and the gap between and could well be within the noise at 0.013. In that post, I trained three models with different weight initialisation seeds, and got models that differed by up to ~0.017. The two models with the corrected smart initialisation are the worst -- even worse than the model with no extra initialisation, . LoRE can reduce the number of parameters in these models dramatically even if only applied to the input embeddings, and that comes with potentially an improvement in test loss (0.073 in one test, 0.013 in a second). When applied to the output head, it has the same size of reduction in the parameter count, and causes a worsening in test loss (over three tests, 0.115, 0.138 and 0.186). The results with LoRE on both ends seemed to come in somewhere around (in two of the three cases, very close to) the sum of the input-only and output-only deltas, though it doesn't seem to be a strictly additive relationship. The mathematically cleaner implementation of what I've been calling "smart initialisation" actually worked worse than the mistaken version I used originally, though this was only tested with one seed, so the evidence is much weaker. Against my own GPT-2 style model (important differences from the original: no weight tying or bias on the QKV weights, no dropout, and PyTorch default weight initialisation). With two seeds. With two options for smart initialisation, and one of them only with one seed. Over a number of tokens chosen to be Chinchilla-optimal for the baseline non-LoRE model. 7 Maybe the effect was just limited to the seeds I tested? Two is better than one, but three would be better still, four even better, and so on. Maybe the effect disappears in longer training runs? Perhaps LoRE causes some kind of loss in capacity that stops models from improving past some point. Intuitively that could make sense -- if you imagine training as being in some sense compressing information from the training data into the parameters, having fewer parameters is clearly going to limit your capacity in some sense. Isoparameter tests: Input-only LoRE saves 32M parameters, so what happens if you "spend" that on extra layers? Or alternatively make the model wider (in terms of its embedding dimension)? Or some combination of both? Output-only LoRE likewise. And, of course, both input and output. Isocompute tests. Notably, input-only LoRE doesn't save you much compute, as I mentioned earlier -- embedding layers are cheap in terms of compute, if not in terms of parameters. So here perhaps it would be more interesting to see what happens if you did output-only LoRE, but trained the model on more data so that the total training compute budget matched. Would you gain back the lost loss? This is often written Z = X W T to reflect the fact that weights are generally kept in d out × d in format, at least in PyTorch, but that's really an implementation detail .  ↩ I'll write more about LoRA in the future -- I've been playing with it a bit -- but essentially, what you do is: Freeze all of the matrices that make up your parameters (eg. in PyTorch, set to ). For each matrix that you want to train (which might not be all of them -- for fine-tuning, people often only train a subset), you add on a low-rank adapter , which is a pair of matrices like our A and B above, and which sits "beside" the existing one, like this: Gradient tracking is enabled on the matrices in the low-rank adapter, and its results are added to the results of the original weights. When I was discussing this with an LLM -- sadly I've forgotten which -- the softmax bottleneck came up here, as it did in later correspondence with Andrew. That's a reference to this paper . I'll need to work through it carefully at some later point, but the relevant point appears to be that the rank (which we can loosely read as how many independent ways the predictions can vary from one context to another) of the values coming out of softmax is limited by the rank of what is going into it. If we force our (in my GPT-2 small case) 768-dimensional embeddings through a 128-dimensional bottleneck, we're reducing their inherent rank, and it's that reduced rank that will drive softmax's, so the results will be worse than what you'd get with the original 768. Seems logical enough. Linkrot-proof reference: Yang, Z., Dai, Z., Salakhutdinov, R., & Cohen, W. W. (2018). Breaking the softmax bottleneck: A high-rank RNN language model. In International Conference on Learning Representations (ICLR) .  ↩ Thanks to Claude Opus 5.5 for pointing me at the central limit theorem. I definitely need to brush up on my statistics, and I'm sure I knew about it at some point back in the 90s...  ↩ Modulo CUDA jitter of various flavours -- though even then, a while back I did two training runs on 8x A100 machines with the same config, months apart, and the Safetensors files were identical bit-for-bit. So I think the effect of that in my setup is minuscule.  ↩ The temptation to dig into the details of why, and exactly what the mistaken smart initialisation did to the variance of the "virtual" weights W ′ , is strong. But I will resist.  ↩ When I ran a draft of this post past my editorial board of LLMs , Grok made the point that perhaps the apparent benefit of having LoRE only on the input embeddings might have been due to that model seeing significantly more tokens per parameter. It's an interesting thought! If we do the maths, the input-only and output-only LoRE models were trained on ~25 tokens per parameter and the both-ends ones were trained on about 33, vs 20 for the non-LoRE ones. However, in my Chinchilla experiments, I only got 0.09 improvement in loss by training on 40 tokens per parameter rather than 20. Now, I'm sure that gain mostly happened early in the run -- overtraining is subject to diminishing returns -- but the result of 0.073 for input-only LoRE would imply that almost all of it happened in the first extra 5 tokens per parameter, which seems dubious. Those are different training runs with different seeds, and were using my JAX code, which has a better baseline loss than my PyTorch code, so we can't compare them directly. But it feels unlikely that the effect would be drastically different. Also, if we use reductio ad absurdum on Grok's logic, it does sound a bit weak -- if we get rid of parameters but train on the same number of tokens, the higher tokens per parameter will not in general counteract the damage from the smaller model. Imagine, for example, removing 32M parameters worth of Transformer layers and training on the Chinchilla-optimal tokens for the size of the model before you did that. I'm not going to run the experiment, but I'd be... somewhat more than surprised if it improved the model.  ↩

0 views

Premium: The Hater's Guide To Junk

Ladies and gentlemen, we are in a glorious, splendiferous, outrageous era of crap!  Some call it “high-yield,” some call it “speculative-grade,” but to those of us living in the real world, we know them as junk bonds, the formerly-sleepy world of below-investment grade debt that’s exploded in the last six years.  Since the beginning of 2011, junk bond issuance has increased by seventy-five times , from a mere $3 billion issued against $60.8 billion in investment-grade bonds in the first half of 2011 (around 5%) to an astonishing $229 billion of junk against the $805.9 billion in the first half of 2026 — making the high-yield market about 28.4% the size of the investment-grade market. The high-yield market has ballooned over the last few years thanks to the vagaries of the global economy and, in recent years, the arrival of an entirely new category of crap.  And “junk,” in the case of today’s newsletter, is going to extend so much further than simply “high-yield,” and into the murky world of leveraged loans that have been used to fund dodgy software deals and an increasing amount of data center debt deals. So why should you give a shit about junk?  As I covered in this week’s free newsletter , Anthropic and OpenAI are two of the single-worst businesses in the history of capitalism, with negative EBITDA cashflows and massive customer concentrations, making them likely to be rated toward the lowest tiers of junk — CCC, or the equivalent rating in Moody’s system, Caa: While you probably know this, “default” refers to when a company has missed a payment on its debt and the credit agencies don’t believe that it will ever make that payment.  The AI labs will require $50 billion to $100 billion of annual issuance across the worlds of high-yield, private credit, leveraged loans (high-interest loans with floating rates issued to companies with a ton of existing debt), and revolving credit lines that, according to a source in fixed-income, are the kind of thing you only use as a last resort. They’d also be the first parts of the AI industry to truly touch the world of junk other than the disgraceful AI neoclouds, companies that raise oodles of debt with the vague promise of building AI data centers some time in an indeterminate future, but serve the more immediate benefit of pumping NVIDIA’s revenue numbers by buying GPUs years before they’ll ever dance with the power grid.  Regardless of how shitty it is, this industry needs hundreds of billions of dollars to fund the theoretical buildout of these potentially-possible data centers — CoreWeave alone, per UBS, needs to raise $102 billion in debt through 2030 — at a rate with no historical comparison. Even the railroad bubble of the 1800s had, based on rough calculations of inflation, only around $250 billion in total investment compared to the $400 billion in issuance expected from hyperscalers alone in 2027 . Yet the vast majority of companies building AI data centers range from low credit to no credit, with whatever creditworthiness they may have based near-entirely on their proximity to either NVIDIA or one of the hyperscalers that is invariably going to be their customer. The problem, you see, isn’t really the AI of it all, but the uniquely stinky business of being in AI. Even under the best possible circumstances, an AI data center will need billions of dollars up front, years in advance of any potential return on investment, buoyed only by the hype around the potential payoff at the other end.  All of this exists in a time in history when more and more companies are demanding more and more debt from the markets — including the large, wet son of Larry Ellison and his $52 billion bond/loan sale to fund their takeover of Warner Brothers Discovery , $12.4 billion of which was funded with junk due to the sheer scale of the buyout, with Paramount/Skydance/Whatever paying as much as 9.1% on the 10-year end of the deal.  And as I’ve discussed in the past , Larry Ellison’s Oracle now sits on the very last rung of investment-grade debt , with any further downgrades dropping it into the junk markets and leading to investment and pension funds legally having to dump its debt en masse, which would be a big problem considering the $30 billion or more of personal loans Ellison has collateralized using Oracle stock will face brutal margin calls in the event the stock dumps…which it will absolutely do in the event of a downgrade. Its last downgrade came from the most obvious of places, per S&P Global: Today’s exploration of junk is a culmination of multiple different threads of premium research, ranging from the AI data center bubble to the SaaSpocalypse , with massive amounts of leverage powering some of the worst deals in history, creating a setup for private credit and other investors to lose billions of dollars as a result. Welcome to the Hater’s Guide To Junk, or Enter The Crapverse.

0 views

A new feature for my blog, built using my voice

I shipped a new feature for my blog today: the Newsletters page, which offers an index of all of the newsletters I've sent out, both my free weekly Substack and my monthly sponsors-only updates. I built the feature almost entirely using my voice, chatting away to my laptop while I cooked dinner. I used the ChatGPT desktop app for this, in the Codex tab, using the voice conversation mode, running against a local development environment. Here's what that looks like: I started the session against my local simonwillisonblog checkout by typing: This gave me a preview of the site that it would be working on, and meant that I could later ask it to show me the new pages so I could visually track its progress. Then I clicked the "Start new voice chat" button - that's not the microphone button, it's the one to the right of it - and set my laptop up in the kitchen so I could talk to it while I cooked. I had a pretty good idea of what I wanted to build, and it's a simple enough Django feature that I was certain the model (in this case GPT-6 Astra High) would be able to do it. A new model, a migration, some view code, templates, and a couple of import functions to populate the database from external sources. Here's an extract of my voice transcript that was captured by Codex: Um, they do not. Um, this is going to be a new type of content. Um, it's not going to show up... Oh, hold on. Yeah, no- I do not want this to show up in my, um, tag pages and date archive pages and... Actually, no, I think... I don't want it on the tag pages. I don't want it on the, um, blog index page. But I think I do want it to show up on the date-based pages. You know, if you navigate to September the 19th, and I sent a newsletter on that page, I think I want that to show up. So... this is- so I think we probably need a new model. The other thing is that I want them searchable, uh the Substack ones are not searchable, because those are actually just copies of other s- on content on my blog. These monthly ones do contain unique content, and spe- and once they're... published, like once they're made public a month after they've gone out, I want them to show up on my search results. Apparently this was clear enough that the model knew what I wanted to build! You can read the full transcript, disfluencies and all, in this Gist . We went on like this for about half an hour (the time it took to cook dinner). The model would reply and occasionally ask clarifying questions, then get to work modifying the code. We got a surprisingly long way entirely by voice: It was almost ready to ship. The catch was the imports: Astra offered to export data from my local copy so I could import that into production, but I wanted it to work like my other import scripts. Since some of the data lived in a private GitHub repository, this would involve creating a new API key, and for that I knew I'd have to sit at the keyboard for a while. Once I had finished cooking and judged it mostly feature-complete, I had Codex create a branch and open a pull request. I reviewed the code in the GitHub PR interface. It was nearly what I needed, except it had chosen to use Git in a subprocess for one of the import scripts. I needed one of the imports to pull from a private Git repository, so I figured the API would be a better bet. I switched to typing and had Codex swap that out for an API-based import instead. You can see the changes I made during the review in the extra commits on the PR . I fixed the import mechanism and made a few tweaks to the display of those public pages. It took an additional half hour of typing-based prompting to get to the point where I was happy to deploy it to production by landing the PR. You can see the end result at the new newsletters index page , or view the page for a previous monthly newsletter . The index page shows my most recent Substack weekly newsletters and GitHub sponsors monthly newsletters mixed together in reverse chronological order. Further down the page are links to my by-year archive pages. GPT-6 Astra designed the page, and then tweaked that design based on my vocal feedback from glancing at the local preview across the kitchen. OpenAI love using voice-driven demos like this one for things like DevDay - and they do work well in that environment. I don't think this is going to be a daily driver for me though. I've written before about how much "work" I get done using ChatGPT voice mode on my phone while walking the dog - mostly research and brainstorming, but occasionally actual development work by having ChatGPT write and test out snippets of code. This feels different. The addition of the visual preview, plus being able to type or paste things in via the keyboard when I need to communicate something that doesn't work vocally, makes this a much more powerful way of interacting with a coding agent. I still switch back to typing once I get down to the details of things though. Being able to paste in examples and error messages, or directly highlight the code or feature that needs changing, remains more efficient than trying to describe it in words. I mainly work from home, which is good because there's no way I'd want to talk to my computer like this in a shared workspace! The killer feature for me is the ability to multi-task. I usually cook with a podcast or TikTok running; now I can actually build stuff instead. You are only seeing the long-form articles from my blog. Subscribe to /atom/everything/ to get all of my posts, or take a look at my other subscription options . A new model and migration to represent imported newsletters in Django, plus Django Admin configuration for that Four working imports: The most recent Substack items via RSS Every other Substack item via their undocumented API, which GPT-6 Astra knew about (it tried directly) and then ran a search to figure out how to paginate it and found this article by Karen Spinner All of my published monthly newsletters from my simonw/monthly-newsletter-archive GitHub repository My most recent private sponsors-only newsletter from a private repository The /newsletters/ and /newsletters/2026/ public archive pages Newsletters showing up on day and month archive pages too, but not on tag pages or my homepage Weekly Substack newsletters link to Substack; archived monthly newsletters have their own pages Integration with my site search engine

0 views
Brain Baking Yesterday

Laptop Stickers: Yay Or Nay?

Here’s an interesting dilemma for you: do you place stickers onto the back of your laptop? Are you a laptop sticker kind of person or afraid of anything glossy that might leave glue marks? I used to belong to the latter group, but after more than six years of typing on this M1 Air , I was ready to give in. The reason for this is simple. Sebastián sent me a couple of Emacs-related stickers, knowing I couldn’t resist. It’s all his fault. Look at what he did! A not so pristine golden coloured MacBook Air shining in the sun, desecrated by four stickers. (And yes, I am well aware of the irony of pasting a Free Software Foundation sticker on a MacBook that runs on a proprietary OS. I promise my next hardware choice will be more ethically sound.) Of course I can’t stop there: what to do with all that open space in-between the stickers? I could have placed them all at one side to make it even more painfully obvious that the beautiful symmetry is completely gone now. As for the question of where to stick them: I already think far too much and was too happy with the stickers to give this much thought. They’re on there. The Apple logo is still visible: a Brain Baking logo sticker covering that up might be the logical next step to take. Every time I receive stickers at conventions, I hesitate: do I stick these onto the laptop? Wait, what do they represent? Do I really want to proudly display the Octat GitHub mascot to promote GitHub as “the only way to do Git”? Nope. Do I really want to paste a Java mug or Gopher on there, identifying myself with these programming languages that aren’t bad but don’t get my engine running? How about a colourful JetBrains IntelliJ one that can serve as a free ad? Nope, nope, nope. It was easy to be in the (tech) sticker hater group. And then I finally found something that was fun to mess around with. So yes, I am now a happy Lisp and Emacs advocate at work. The stickers already provoked many Emacs versus Vim discussions that end once you show them that Emacs can be a window manager running your other apps, or that EVIL mode exists. Still, 99% of the die-hard coder colleagues—which are less than 10%, the others of course rely on VS Code—are Vim users. That’s great! But one wasn’t and told me he yesterday closed his Emacs window for the first time in weeks. We both had to move classes but I’ve made a mental note to meet up and exchange Lispy configs. Thank you Seb & Seb’s stickers. Many of my students like stickers on their laptops. Most just stick on there whatever they can get their hands on. I’ve seen a lot of Gophers but nowhere in our curriculum we explore Go and after approaching them, I learn that they don’t even know how to write a line of Go code. A Gopher is cool, that’s what matters! I do think that you should at least know what you’re implicitly preaching. Which is why I’m not limiting myself by sticking only tech-related stuff on there. The question then becomes: what else? Something retro game-related, obviously. But still: what? A classic Castlevania logo? I’d rather go for a custom-printed sticker with some obscure sprite work, from for instance Wario Land 3 or Gobliins 2 . If someone is able to recognise all these, I’ll finally have found my missing soulmate. Maybe a pixelated version of bread or a fountain pen? Or am I giving away too much information that way? Also, since the laptop turns seven in January, I should keep copies as the stickers are not transferable. Another approach would be to cover the entire back, making use of every square millimetre. A few colleague design lecturers carry laptops like this. I don’t think I’m cool enough for that. Terence caught a nasty laptop sticker paralysis while trying to perfectly place his, so a bit of thoughtful preparation might be in order. I love Abigail’s Kirby sticker on her Thinkpad. She even scanned her laptop with a photocopier and converted the entire thing into a clickable polygon-based SVG. Much cooler than my lazy cellphone snapshot. I’m also jealous of her Cory Wong pizza slice sticker! I do wonder what she’ll do when her laptop breaks down or it’s time for a replacement. Nia’s laptop stickers (a November 2022 snapshot) also contains some cool ones, as does Manton Reece’s , such as bookstore stickers. Here’s a discussion on the Framework forum containing more inspiration. It is clear that I still have some work to do. The four stickers are only the beginning. Laptop Stickers: Yay Or Nay? Yay. But then: how many? Overlapping or not? Planned placement or not? Tech-related only or not? See, even the most banal decisions in life come with Deep Thoughts ! To be continued with a photo when it’s done. Related topics: / stickers / By Wouter Groeneveld on 9 October 2026.  Reply via email .

0 views
iDiallo Yesterday

20 Minutes of Political Debate, Brought to You by Commercial Breaks

"I'm sorry, you're out of time, we have to move on. Senator, what's your response? You have three minutes." Watching a political debate these days feels useless. Candidates get two minutes to make their case, and their opponents get even less time to reply. I'm reminded of Amusing Ourselves to Death by Neil Postman, where he argues that what passes for debate on TV is nothing more than an audition or a performance review. It is only an opportunity to come up with catchy sound bites or to appear likable. On the other hand, if you want long-form, one-sided podcasts where politicians can babble uninterrupted for hours without being challenged, you can tune into Joe Rogan, Lex Fridman, or whichever pseudo-comedian is trending. Our choices seem locked between traditional media, where you barely have time to clear your throat, and one-sided online echo chambers. So why not a third option? Two candidates sitting down in a long-form podcast format. Debate the issues, prove your point, and take turns. No commercial breaks required. If it takes three hours, it takes three hours. This format isn't new, in fact, it plagues social media right now. The problem is that it's mostly driven by influencers, or people of no consequence, chasing viral moments. They are either doing gender wars, or arguing whether it was a Nazi salute or not. When you switch to traditional media, the talking heads on CNN, Fox, or Piers Morgan's show are just that. Talking heads. Of course, this might never happen because candidates have almost zero incentive to subject themselves to it. If they're unprepared or rely on weak arguments that don't hold up past a 15-second clip, a three-hour deep dive could destroy their campaign. Still, it would be nice to see Michiganders give this a shot in the coming month.

0 views
Michael Lynch Yesterday

Why Are Coding Agents So Dumb?

The first time I used a coding agent, I was mesmerized . Before the agent, I was copy/pasting between my IDE and an AI chat interface. It was amazing to see an agent edit files directly and fix its own errors in real time. After a few days, the honeymoon wore off as I encountered frequent bugs. The agent would stop responding entirely until I restarted it. Development workflows felt stiflingly primitive, and the agent would often declare tasks finished when work had barely begun. This was in February 2025, so it was still early days for coding agents. I figured that in six months, agents would be as technically impressive as the underlying LLMs. Instead, coding agents just stayed bad. AI-assisted development has clearly advanced, but the models are doing the heavy lifting while the agents remain the bottleneck. In all the hype around AI, the terms tend to get distorted. People are beginning to overload and mix terms like “model” and “agent.” When I say “model,” I’m talking about large language models (LLMs) like GPT Astra, Claude Sonnet, and GLM-5.3. Models generate text and images, including pretty good software code. When I say “agent,” I mean the software that connects models to codebases and computer systems. These are tools like Anthropic’s Claude Code or OpenAI’s Codex. As a simple analogy, the model is the brain, and the agent is the body. The model produces a stream of text, and the agent acts as the glue that plugs the text into the right commands and files on the system. My biggest gripe with coding agents is how atrociously they manage tasks. For example, I have an open-source web app that generates shareable links for file uploads. I recently added support for protecting links with a passphrase . It was a relatively simple change, totalling about 1.5k lines of new code. OpenCode dutifully broke the feature into 10 subtasks, but then it just… did them all one by one: Why are you doing these embarrassingly parallel tasks one at a time? Umm… you’re a computer ! You’re really good at multitasking. That’s why we keep giving you all those CPU cores. You can do multiple things in parallel and context switch millions of times faster than humans. Why are you doing these embarrassingly parallel tasks one at a time? Claude Code multitasks, but only a little. It will spin up a subagent or two, but it still waits for all of them to finish before moving on. Multiple times per day, I’ll see Claude Code sit around for several minutes waiting for my end-to-end tests to finish, and then only after the tests pass does it say, “Hmm, now I should start drafting a commit message. Let me look at the git history to learn your commit message conventions .” When I’m using a cutting-edge model, and it needs to check 50k lines of code for a particular pattern, the agent never stops and says, “Wait, this is something another model could do cheaper and faster.” It just plows on with the slow, expensive model. Conversely, the agent never says, “This model is too dumb for this task. Let me tag in a smarter one.” Of course, I can actively micromanage the task and keep switching the model and thinking level to match each subtask’s difficulty, but why is that my job? Do you also need me to manage your thread pool for you? Do you expect me free your unused RAM for you, too? You know what technology would be good at assigning a difficulty level to a task and then matching those requirements to a model? An LLM! Just ask the LLM to pick the cheapest, fastest model for the task. Why do you need me to babysit you? I constantly run into tasks that are 95% gruntwork, but I still have to assign them to the smartest model because chopping up the task and delegating on the agent’s behalf would take up too much of my time. Thanks for telling me which is the default model, Claude. Agents don’t know anything about themselves. If I ask Claude how to use the features of Claude, it has to search online to figure out what this “Claude” thing is. Claude is more comfortable answering questions about C programming than talking about itself (in fairness, same with most human developers). Uh… you’re Claude Code! You don’t know any of your own freaking features? And you’re just Googling instructions regardless of whether they match your version number? You’ll casually download 13 GB of files for a feature the user has never used, but you can’t spare 50 KB of gzipped text in your install package to explain your own features to you? Imagine if you asked your teammate for a code review , and they started furiously Googling to find out if code reviews are something developers do. And then when you asked them for another code review the next day, they had no memory of your previous conversation and ran back to Google and anxiously typed, I used to love the agent UX feature of separate “Plan” and “Execute” modes. For complicated tasks, I’d ask the agent to create a plan, then I’d review it, suggest changes, and delegate execution to a faster, cheaper agent. Over time, I felt an aversion to reading the plans. I’d often skip my review and just let the agent move straight to implementation. I thought coding agents had made me lazy, but I realized that agents just communicate their plans so poorly that they’re painful to read. Here’s an example of me asking Codex + GPT-6 Astra to add a feature to my media journalling web app : You can’t just list a bunch of disparate details and call it a plan, Codex. That’s not a plan! That’s just a hodgepodge of low-level design decisions. If I asked a competent developer to plan this feature, they’d either start with a high-level plan for UI changes and work their way down or describe changes to the data model and work their way up. If the developer started enumerating random facts about the feature, I’d assume they were brainstorming and come back later. The other night, I kicked off a long task in a coding agent before I went to bed. I came back the next morning to find that the agent hadn’t even started working. It stopped two minutes after I left to ask me what it should name a git branch and then sat all night waiting for my answer. If I had a human employee tell me they sat idle their whole shift because they wanted my input on some superficial detail, I’d quickly fire them. When I started using my first coding agent, I looked for the setting that controlled which files on my system the agent is allowed to access. Surely, there was some sort of filesystem permissions or limited chroot kind of protection that prevents a random and unpredictable piece of software from exploring my entire computer unfettered, right? Not so. The docs encouraged me to write the LLM a polite letter kindly requesting that it not read certain files or directories. I tried that, and the agent immediately ignored my request, exfiltrating private application keys to OpenAI and Anthropic. I thought that security boundaries would be one of the first things coding agents would implement, but even today, agents are only usable if you give them access to everything. Agents routinely bypass their own vendors’ sandboxes . The alternative is to sit there and click “Allow” 500 times a day, and that’s not even reliable protection because you’re bound to misclick eventually. What makes this so maddening is that we’ve had sandboxing tools for more than a decade that can limit the blast radius of mistakes from coding agents. I rolled my own sandbox so that agents can’t explore my filesystem beyond the repo directory. I never have to worry about agents accidentally exfiltrating my home directory or wiping critical files on my machine because they just don’t have access to do that. I know some readers will say that I can solve all of my problems if I just install 200k lines of skill files from random git repos or set some obscure feature flag in my config file. I’m talking about my expectations of what coding agents should be able to do out of the box without me installing random plugins or skill files or spending hours tweaking the configuration. These are the basics that I think should be table stakes for coding agents in 2026. As long as I’m dreaming, here are some additional features I’d like to see, but I recognize that some of these are overindexing on my personal workflows. Okay, getting back to the question in the title, I don’t have a satisfying answer. My best hypothesis is that underinvestment in coding agents is an example of the principal-agent problem . The people setting the direction of AI tooling are executives at companies like Anthropic, OpenAI, and Google. Those executives are disconnected from the rank-and-file developers who use coding agents every day. Many of these executives are dreaming of a future where they can automate away human developers entirely. AI executives, as well as their largest customers and shareholders, pay attention to metrics that are legible to them, such as slick demos and benchmark scores. Security and efficient use of human developer time aren’t relevant to the demos, and barely any of the benchmarks I’ve seen measure the agents themselves; they just measure the underlying models. My hypothesis isn’t satisfying because AI companies clearly care at least a little bit about coding agents. I see a lot of features being added to Claude and Codex every month, though I can’t recall the last time one of them has improved my life. I’ve only tried Claude, Codex, OpenCode, Cline, and Pi. I use OpenCode and Claude Code as my daily drivers. If you’ve got a coding agent recommendation for me, comment below. AI companies - if you want to acquire my imaginary coding agent for $50B, let me know. I’m ready to fork VS Code at a moment’s notice. The agent splits requests into a series of tasks and assigns each task to the appropriate model. The agent optimizes for cost, speed, and correctness and allows the user to adjust the dials per task (e.g., spend more for a faster result). The agent writes plans that optimize for human comprehension. The agent starts at a high level of abstraction and progresses toward the minutiae . The agent creates UI mockups, data flow diagrams, and decision trees . The agent operates within a real sandbox. The sandbox uses OS-level security primitives to create boundaries at the filesystem and networking level. All access control code is deterministic, not humble suggestions that the agent is welcome to ignore. If I ask the agent whether a list of regexes on bash commands is a sandbox, it replies, “No.” The agent applies per-environment sandboxing. The agent has access to a single repo/directory by default. I can give the agent read-only or read-write access to other repos on a per-session basis. The agent is an expert on itself. If I ask the agent how to express a task or workflow to the agent, it knows the answer without having to search online. The agent can use any LLM provider, including unlimited plans. The agent is open-source. If I don’t answer a question in “Execute” mode, and I haven’t interacted with the session in 30 minutes, the agent makes the decision independently. The agent also offers an “AFK mode,” which skips the 30-minute wait. The agent lets me drive the subagents, too. I should be able to jump into any agent session and drive it or tell it to short-circuit and end early. If the agent tells me that Fable is not available on my Max plan , the agent vendor’s CEO must remain in stockades until the bug is fixed. The agent offers a web interface that shows me a unified view of all sessions and which ones require attention. The web backend runs locally and doesn’t require me to open a tunnel from the Internet that executes arbitrary commands on my system. The web interface works well on my phone. The agent maintains an ETA for task completion. Each subagent maintains its own ETA as well. The agent continuously updates this estimate as the task progresses. The agent tunes its estimation algorithm based on the accuracy of its past estimates. The agent reviews its own sessions and looks for opportunities to improve. e.g., “Wow, I blew through $1k/day in tokens the past five days trying to parse this 20 GB log file with ad-hoc commands. Let’s build a custom tool to do this efficiently.” The agent comes with a good language-aware diff view. I don’t want to have to push to GitHub to see a useful diff of the agent’s work. The agent natively supports a proxy for injecting secrets into network requests. The agent can make requests that require credentials but can’t exfiltrate the credentials to another host. The agent considers provider quota limits when selecting an appropriate model. e.g., if my weekly quota resets in 3 hours, and we still have 90% of quota available, stop optimizing for cost. For tasks above a configurable complexity threshold, the agent automatically requests a code review from another model. The two models iterate on reviews until they converge on the fixes.

0 views
Ahmad Alfy Yesterday

Iframes that finally fit their content

Chrome 154 lets an iframe grow to the height of its content with one line of CSS without having to measure, without messages, and without resize scripts. But the page inside the iframe has to agree to it. That catch is the most interesting part of this feature, so this article spends some time on it. I have built many checkout pages that use a payment provider’s iframe. The goal was always to have the card form feel like part of the page. The user should not notice that it comes from another website. The iframe never helped with that. It has a fixed height. Make it too tall and you get an empty gap under the form. Make it too short and you get a scrollbar inside the page’s scrollbar. On mobile, that second scrollbar is the worst thing you can show someone who is about to pay. So I kept increasing the height, testing on different phones, and increasing it again. This is a small problem. It should have a small solution. For years it did not. The parent page cannot look inside a cross-origin iframe. It does not know how tall the content is. So the only way was to make both pages talk to each other with JavaScript. Inside the iframe, you measure the content and send the height to the parent: In the parent page, you listen, check who sent the message, and set the height: This looks short, but it hides a lot of problems: That last point did not go away with the new feature. It just moved into the browser. In the parent page, you add one CSS property to the iframe: Inside the iframe, the page opts in with a meta tag in its . It also says which websites are allowed to size it: That is all you need for content that does not change after it loads. The browser measures the content and sizes the iframe. No messages, no listeners, no origin checks in your code. The meta tag must be in the HTML from the start. Adding it later with JavaScript does not work. If the content changes later (an error message appears, a section expands, more comments load), the page inside the iframe asks the browser to measure again: So JavaScript does not disappear completely. The embedded page still calls one function when its content changes. But the hard parts are gone. The browser does all of that now. also accepts , and . For most pages, is the one you want. You can still combine it with limits like . This is the use case I care about most, and it is also the one that depends most on someone else. A payment form changes height all the time. An error appears under the card number. The user switches from card to wallet. A saved card list shows up. With , all of this could look smooth inside your checkout. But you cannot turn it on from your side alone. You control the CSS on your checkout page. The payment provider controls the page inside the iframe. Only they can add the meta tag, list the merchant sites that are allowed, and call when their form changes. So for payments, the real question is not “does Chrome support this?” It is “does my payment provider support this?” Today, most providers either ship their own postMessage script or do nothing. If you work with one, ask them. If you build one, this is a cheap win for every merchant using you. Comment sections, contact forms, newsletter sign-ups and booking widgets all have the same problem. Their height depends on the content: the number of comments, the number of fields, the validation errors. These services already control their embedded page, so adding the meta tag is easy for them. The list fits well here, because they already know which customer sites embed them. I have this exact problem on this website. My contact form is a Wufoo form inside an iframe, and I set its height by hand until it looked right. Each step of a form has a different height. Step one has two fields. Step three has ten. Today, you either reserve space for the tallest step or let the iframe scroll. With this feature, the form calls after each step and the iframe follows. This one does not need any third party. Many apps show HTML email previews, rich text previews, or code demos inside a sandboxed iframe using . Here you write the embedded HTML yourself, so you can add the meta tag directly. This is probably the easiest place to start using the feature today. Browser support. This is Chromium-only for now. Firefox and Safari do not support it yet. Keep a fixed height as the default and switch to content sizing only where it works: Inside the iframe, check before calling the new function. Your old postMessage code can stay as a fallback until support grows: Layout shift. The iframe loads after your page, then grows. Anything below it moves down. If the iframe is in the first screen, this can hurt your Core Web Vitals. A sensible reduces the jump. Do not use without a reason. Letting any site read your page’s height can leak information. For example, a page that is taller when the user is logged in tells the parent something about that user. List only the sites that need it. This works together with the CSP rule, which controls who can embed you at all. For years, a simple layout need, “make this box as tall as its content”, required two scripts on two websites that had to agree on a message format. Now it is one CSS property, one meta tag, and one function call when things change. The browser side is ready in Chrome. The rest depends on the people who build the pages we embed. If you run a payment gateway, a comments service, or any widget that lives inside an iframe, add the meta tag. Your users’ checkouts and pages will feel like they were built as one piece. I will come back to payment providers in our region specifically in a follow-up post. Width changes height. On a small screen, text wraps more and the content gets taller. Every resize or phone rotation needs a new measurement. Content arrives late. Fonts, images and error messages load after the first measurement. The height is wrong until someone measures again. Dynamic content. If the page inside the iframe shows or hides elements after the initial load, the height changes and needs to be measured again. More than one iframe. If the page has several, you need IDs in every message to know which one to resize. Both sides must cooperate. If the third party does not send its height, there is nothing you can do. You go back to guessing a fixed height. Responsive iframes in Chrome 154 , Chrome for Developers New in Chrome 154 , Chrome for Developers

0 views
Unsung 2 days ago

Deeper dive: Keyboard differences between Windows and Macs

Over the years, I learned about many gotchas and strange differences between keyboard handling on Mac and Windows – pertinent especially to web apps, which use the same codebase to cater to both. I thought it might be helpful to someone if I compile them all in one place. This post is meant to be a reference, and there aren’t any cute or riveting stories hiding inside – if this seems boring to you, feel free to skip to the next one! What Windows calls Backspace, Mac calls Delete. What Windows calls Delete, Macs call Forward Delete. (This means saying “Delete” without specifying the platform might actually be confusing.) What Windows calls ⏎ Enter, Mac calls ⏎ Return. However, Macs also have an ⌤ Enter, although only on a numeric keypad (previously, it was even there on laptops !). On keyboards without the physical Enter key, you can simulate it via Fn+Return. In most Mac software, Enter and Return do the same thing. There are a few exceptions – for example, Photoshop enters a new line on Return but commits on Enter, and some classic pro apps like Cubase or Pro Tools do different things, too – but it seems to be a dying tradition. (If you are curious about the history of Return and Enter, I wrote about it once .) Windows customarily calls the secondary key Numpad Enter. I don’t believe Fn+Enter works to simulate it. Generally, third-party keyboards use Windows verbiage – so, Backspace and Enter. If a keyboard offers Mac conventions at all, they usually only extend to modifier keys. ⌃ Control on Windows is the equivalent to ⌘ Command on a Mac. (Paste, for example, is ⌃V on Windows and ⌘V on a Mac.) But, confusingly, Apple devices still have a Control key, too. This was originally meant for terminal applications, but these days many GUI apps use it as an extra modifier key. This means that for apps, Windows devices offer Ctrl, Alt, and Shift – and Macs offer ⌘ Command, ⌥ Option, ⌃ Control, and ⇧ Shift. That’s one more modifier key, and thus more space to breathe. (We’re not counting the Windows key or the 🌐 Globe/Fn key since those are technically reserved by the operating system.) Some keyboards offer extra key caps you can swap to match the platform, for example: = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/1.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/1.1600w.avif" type="image/avif"> = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/2.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/2.1600w.avif" type="image/avif"> Others cover all the bases on fixed key caps, in an awkward way: = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/3.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/3.1600w.avif" type="image/avif"> = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/4.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/4.1600w.avif" type="image/avif"> Many stick with Windows-only legends. Apple devices rely more on symbols on their keys and in their menus, although they don’t do so consistently. Here are all of them: Actually, I lied about the last four. On modern Apple keyboards, they are: Reusing the regular arrows for Page Up and Down is one of a few perplexing decisions from Apple’s keyboard designers. The arrow key symbols look like this – ◀▶▲▼ – but only on Apple keyboards. Here is an older and a newer Apple keyboard showing what happened: = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/5.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/5.1600w.avif" type="image/avif"> = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/6.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/6.1600w.avif" type="image/avif"> (Luckily, the confusing dual arrow key situation only happens on less popular, full-size keyboards.) Historically, Apple keyboards used symbols more on non-US keyboards, but starting with the 2026 models, they unified when they show symbols and when they show symbols and legends, across all keyboards. (The only key with just a text legend is Esc, making the appearance of ⎋ in menus extra puzzling.) Windows keyboards typically use words – this is why in tight quarters you sometimes see shortenings like Ctrl, Bkspc, PrtSc, Del, PgUp, Win, and so on. (I don’t think Apple ever abbreviates their legends with the exception of Esc for Escape.) In some countries, the legends are translated – as an example, in Germany, Ctrl sometimes appears as Strg. The symbols that crossed over to Windows side are: I have not seen any other popular symbols on the Windows side of the aisle, and I am not even sure if the above would be widely understood. But here’s an example: = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/7.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/7.1600w.avif" type="image/avif"> ( I wrote a bit more about Mac symbols before , and also about the rare Canadian symbols .) In menus and other places, Windows joins the key combinations/​shortcuts with a plus, but Apple just glues them together: Here is the same Chrome menu on Windows and on macOS: = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/8.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/8.1600w.avif" type="image/avif"> = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/9.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/9.1600w.avif" type="image/avif"> (In other words, you’d never say “⌃V is Paste on Windows” like I did above.) Both Windows and Macs have function keys. On Windows, traditionally those were claimed by the operating system or the apps as shortcuts. Here are some examples of well-known function key assignments: On Macs, traditionally the apps didn’t reach for function keys, as those were reserved solely for the users to do stuff with. (However, some combination of ⌃ and function keys are used by the operating system for accessibility options, and I occasionally see apps use function keys these days.) Windows keyboards top off at F12, but some Mac keyboards reuse the three special PC keys, and even take over the unnecessary Num Lock/​Caps Lock/​Scroll Lock island, and end up going up to F19: = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/10.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/10.1600w.avif" type="image/avif"> Access to extra characters In text fields, Apple has a system where pressing ⌥ with printing keys outputs more characters, for example ⌥Q outputs œ, and ⌥7 outputs a ¶ pilcrow. Additionally, ⇧ works in this context, so for example ⌥⇧Q outputs Œ, and ⌥⇧7 outputs a ‡ double dagger. = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/11.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/11.1600w.avif" type="image/avif"> Note that not only letters, but basically all printing keys have secret ⌥ and ⌥⇧ assignments. Also, ⌥ assignments vary per location! The above was U.S. English, here’s Polish with a lot of differences: = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/12.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/12.1600w.avif" type="image/avif"> This means it’s best to avoid ⌥-based shortcuts in text fields, since they might conflict with some important character. By the way, while the above two are just mock-ups, on some physical keyboards (here: British English), some of the important ⌥ invocations are actually printed on keys: = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/13.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/13.1600w.avif" type="image/avif"> Windows doesn’t have the above feature. However, Windows has an alternative feature where typing Alt+numpad keys allows to enter any character by its code. (For example, Alt+0128 outputs €. Num Lock has to be enabled. I don’t think it’s possible to do it without a numeric keypad present.) Mac has a version of this feature, but it requires adding Unicode Hex Input keyboard and switching to it beforehand. Then, pressing ⌥20AC outputs €. While Mac modifier keys are completely symmetrical, Windows makes an exception for Alt. On many non-US keyboards, right Alt is also known as AltGr , and does something similar to ⌥ on a Mac: it outputs letters when pressed in combination with printing keys. For example, on Polish keyboards AltGr+A = ą, AltGr+C = ć, AltGr+Shift+A = Ą, and so on with 15 more combinations. Many other keyboards do similar things. The way it differs from ⌥ on a Mac is that these are usually reserved for core letters and punctuation necessary for each language, rather than the typographical smorgasbord that Apple provides. For legacy reasons, and also for keyboards that do not have a physical AltGr key, you can also invoke all these using Ctrl+Alt combinations instead (so, Ctrl+Alt+A = ą). This means that just as you have to be careful about ⌥-based shortcuts in text fields on a Mac, so you should be of Ctrl+Alt-based shortcuts on Windows . Just like on Macs, on some keyboards, selected AltGr options will be printed in the corners or fronts of keys: = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/14.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/14.1600w.avif" type="image/avif"> Text fields Text fields in Mac OS apps and web browsers/​websites use some of the standard Unix/​Linux shortcuts based on the ⌃ Control key: You can combine many of the above with holding ⇧ to extend the selection. A small group of vocal users love these. Windows still supports Ctrl+Insert for copy and Shift+Insert for paste. I am not sure if those are being used. On a Mac, in simple input fields, ↑ and ↓ jumps to the beginning and end (same as ⌘←→). This often conflicts with command line history, autocomplete pop-ups, and so on. Windows doesn’t have this convention, and Home and End serve this purpose instead. Macs support the iPhone-inspired convention of holding a key to show related accented characters, instead of triggering auto-repeat. Windows doesn’t have this feature. = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/15.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/15.1600w.avif" type="image/avif"> Differing shortcut conventions worth knowing about On a Mac, redo is typically ⌘⇧Z. On Windows, it’s typically Ctrl+Y. On a Mac, refresh (in browsers, etc.) is typically ⌘R. On Windows, it’s typically F5, although some browsers now support Ctrl+R, too, presumably since function keys are harder to access than they used to be. Windows’s eponymous ⊞ Windows key is reserved solely for the use of the operating system, and so is Mac’s 🌐 Fn/​Globe key. (Although I am not 100% sure of that as I found one place you can create 🌐 shortcuts as a user – I’m just not certain if it’s intentional.) However, each platform also has a lot of shortcut combinations that are effectively unavailable, for example ⌘⇥ and ⌘M on a Mac, or Alt+Tab and Ctrl+Shift+Escape on Windows. These official lists can help: If you’re a web app, you will compete for shortcuts with the operating system (like any app would), but also with the browser itself. You can typically take over shortcuts like ⌘S or ⌘P, but depending on the browser or the platform, some might be sacred and unavailable. No Mac browser will allow a website to claim ⌘Q, ⌘W, or ⌘T. Safari won’t allow a web app to override ⌘R. Arc browser won’t allow to override ⌘⇧C. (This is not a complete list.) Tabbing and Shift tabbing is customarily used to jump between UI elements, but it behaves slightly differently in native apps. On Windows, tabbing jumps through all elements: On Mac, Tab jumps only to elements that require keyboard to operate (such as input fields). You can toggle a System Settings preference and ask macOS to mimic Windows behaviour – see the last toggle below – but it’s not supported well everywhere. = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/18.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/18.1600w.avif" type="image/avif"> PgUp and PgDn work differently: Similarly, Home and End work differently: On both platforms, Fn+↑↓ does PgUp/​PgDn, and Fn+←→ does Home/End. (Do you see how confusing it is to say that given that ↑↓ already mean PgUp/Dn on a Mac?) Windows has a tradition of enabling access to menus and visible controls by pressing Alt and letter keys. This has evolved over time and is not as consistent as it used to be, but it might be worth knowing about. On a 100-plus-key keyboard, Windows might have: = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/19.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/19.1600w.avif" type="image/avif"> Macs have: = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/20.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/20.1600w.avif" type="image/avif"> Macs never had arrow keys on a numeric keypad nor a Num Lock key to enable it. (I’m breaking my promise! Here’s a fun bug story about Num Lock .) In a strange twist of fate, it’s not only third-party keyboards that favor Windows legends. Some of Apple’s keyboards in between 1980s and 2000s showed PC legends, too! (This was to court PC compatibility of then-beleaguered Macs.) Here’s the classic Apple Extended Keyboard, showing legends for Insert, Delete (naming it Del to avoid confusion with its own), Print Screen, Scroll Lock, Pause, Num Lock, and Alt: = 2x) and (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/21.2096w.avif" type="image/avif"> = 3x) or (width >= 700px)" srcset="https://unsung.aresluna.org/_media/deeper-dive-keyboard-differences-between-windows-and-macs/21.1600w.avif" type="image/avif"> (Did I miss anything or make a mistake? Let me know !) ⎋ Esc (not printed on keyboards, for some reason) ⌦ Forward Delete ≣ Contextual Menu (only on full-size keyboards) ⇞ Page Up (only on full-size keyboards) ⇟ Page Down (only on full-size keyboards) ↖ Home (only on full-size keyboards) ↘ End (only on full-size keyboards) ↓ Page Down ⇧ for Shift ⇪ or 🔒 or a similar symbol for Caps Lock (on non-US keyboards) ⏎ for Enter – note the same arrow as Mac’s ⏎ Return ← for Backspace – note a different arrow than Mac’s ⌫ Delete ⇥ for Tab (you can also sometimes see ⭾, which is a symbol representing Tab and Reverse Tab together; Reverse Tab used to be a separate key on some 1970s terminals) ⊞ for Windows key – the style of the logo will be different depending on the age of the keyboard, roughly matching the Windows logo at the time; some keyboards also use a more abstract shape, or call the key Start or System instead of Windows ≣ for contextual menu key (a.k.a. Application Key) – just as Apple added that key on its large keyboards, Microsoft started removing it in favor of emoji key , Office key , and then Copilot key ⌃ for Control (especially in nerdy contexts) Windows: Shift+A, Ctrl+Shift+G, Ctrl+F11, Alt+Enter Mac: ⇧A, ⌃⇧G, ⌘F11, ⌥⏎ Alt+F4 – close the app F11 – maximize window F12 – dev tools in browsers ⌃A – move to the beginning of the line ⌃E – move to the end of the line ⌃F – move to the right, or forwards (hold ⌥ to jump through words) ⌃B – move to the left, or backwards (hold ⌥ to jump through words) ⌃N – move down or to the next command ⌃P – move up or to the previous command ⌃L – scroll the window so that the text cursor is in the vertical middle ⌃H – delete (backspace) ⌃D – forward delete ⌃K – delete (kill) to the end of the line ⌃T – swap (transpose) the adjacent characters ⌃O – insert new line, but (contrary to Return) do not move the cursor there Mac keyboard shortcuts Keyboard shortcuts in Windows On Windows, they move the text cursor a screen up or down. On a Mac, they scroll the view up and down, but they do not move the text cursor if it’s present (so, they are more an equivalent of clicking on the scrollbar chute). On Windows, they scroll the contents (and move the cursor if present) to the top or the bottom of a view, or move the cursor to the beginning or the end of an input field. On a Mac, in views they scroll to the beginning or end without moving the cursor. In input fields, Home/End do nothing, but you can use ⌘←→ to accomplish the same. Insert – still used in some contexts for overtyping Print Screen – today taken over by screenshotting Num Lock and Scroll Lock Pause/​Break Help – rarely used, and now abandoned in favor of… ≣ Contextual Menu – shows the same menu as right click would ⌧ Clear – a deterministic backspace , these days seldomly different than the actual Delete key

0 views
Jim Nielsen 2 days ago

“Getting off the Modernization Treadmill”

My notes from this talk by Alexander Petros at Big Sky DevCon 2026 . Alex starts by noting how “modernize” used to mean something along the lines of “update this thing that was made before I was born”. But now “modernize” means something more like “update this thing from 5-10 years ago” (hence the framing of the talk, the “modernization treadmill”). Using a real-world example of an incredibly slow website that was required to access state-sponsored programs for welfare, Alex points out the disparity in conditions between those of us who make software and those who have to use them: The people who develop these websites are usually doing so on high-powered internet connections and high-powered devices, but they're not using them in the conditions that the people who most need those benefits are going to be. Then he shows a Reddit thread where somebody essentially posted, “I’m having problems with this website. I’ve been waiting for months for my application to go through. Any suggestions?” And one Reddit user responded, “The best thing you can do is go into the physical office, get a case worker, and your problems will be solved within the hour.” I guess we've come full circle now. It used to be: “Don’t talk to anybody. It’s faster and more convenient to use the website!” But now it’s: “Don’t use the website. It’s faster and more convenient to talk to somebody!” Have we failed at making websites? And is our failure, at least in part, rooted in the fact that we don’t leverage the basic tools for making websites: HTML, CSS, and (in a distant third) JavaScript? Alex goes on to argue that the technologies of the web have an ideological bent and, if used as designed, can solve so many of the performance, accessibility, and usability issues that plague so many websites. The grain of the web’s technologies are rooted in these values: Which means if you use them as intended, they are optimized to deliver outcomes rooted in those same values. So if you like those values and you want those outcomes, use the platform. Take HTML, for example. Here’s Alex: HTML does [performance improvements] for you for free. If you've coded your website in a proper, semantical, structure HTML style, it will just get better over time at zero cost to the people who built that website HTML is your friend. HTML won’t give you up or let you down . HTML will make it difficult for you to make a bad website. Write it in to the requirements of the project you’re doing that it work without JavaScript. Not necessarily that it doesn’t have any JavaScript, but just that the core functionality of the website can happen without JavaScript. If you do this […] you will find that it’s very hard to deliver a bad web page because the structure that HTML requires is one that fundamentally is good for the user, performant, and cost effective. Technologies are imbued with culture, which influences what you do and how you do it. If you can align your ideological beliefs with your technological choices, you might end up with an outcome that aligns with your values — who would’ve thought, eh? A lot of modern software developers come from websites like Facebook, they come from big tech companies [who] fundamentally have a different set of priorities. Their job is to keep you on the website as long as possible so that you consume more ads. But that’s the opposite set of requirements and priorities that the government needs to be doing, which is to build something that is clean, quick, efficient, and gets you in and out as fast as possible. So [I tell people] that the technology they use comes from [an] ideological place. But there are different ideological places that produce different technological results and if we start from those through lines then we can produce services that help people who need them. The ideological principles of the web are well established : users over everything else. If you use HTML as much as possible, you’ll make something that’s as user-friendly as possible on the web. Reply via: Email · Mastodon · Bluesky User-friendly Backwards- and forwards-compatibility Long-term viability Universal accessibility

0 views
fLaMEd fury 2 days ago

Open Tabs September 2026

What’s going on, Internet? If you don’t follow my Bookmarks through the feed , then here’s the bookmarks from September. Enjoy. For more, check out the bookmarks archive, and subscribe to the feeds if you want these as they happen. Hey, thanks for reading this post in your feed reader! Want to chat? Reply by email or add me on XMPP , or send a webmention . Check out the posts archive on the website. MVNDY — THE POWER OF VISION Spend more time on the idea than the tooling. Craft on its own doesn’t change much. I don’t like passkeys I’m not a big fan of passkeys either. I’ve tried them and don’t particularly care for them. Rubenerd: Ban infinite scrolling I’ve never liked infinite scroll. I prefer pagination. I always lose my place in infinite scroll websites. This is my top hate of Discourse. Give me pagination. The Art of Brütal: Inside the Creative Legacy of Sam “Samwise” Didier | MadmadeLabel Fantastic interview with Samwise Didier, the original artist of Azeroth FINDING MUSIC WITH A LITTLE LESS BIG TECH Ways of discovering music when you’re not on DSP’s or social media. I follow local music venues, local online music mags and music writers. Simplest single file webring implementation : Garden of Learning by Juhis Juhis shares how to create and manage a simple webring in a single page. Celebrating One Year on the Small Web Small wins on the small web 😃 Start a Blog Shannon shares how to start a blog 😃 Harry Potter and the Teenage Websites of Yore GeoCities, FrontPage, and diving into creating websites with HTML. Love it. FrontPage was a crutch before Dreamweaver came around. A Creative’s Guide to Personal Websites (Zine) - with words, wonder James hits us with a neat zine angled at those who think they can’t make a website. Such a cool little project!

0 views