Jon Sterling

I am an Associate Professor in Logical Foundations and Formal Methods at the Cambridge Computer Laboratory, and a Fellow of Clare College.

I like categories, domains, and vintage computing.

Public Key

npub1hfga8wmley5fzqtttpeupd8hc6s92rykfmzktm8zfdhu9h8exvqsj9ls8k

NIP-05 Address

jonmsterling@mathstodon-xyz.mostr.pub

Profile Code

nprofile1qqst55wnhdluj2y3q944su7qknmudgz4pjtya3t9an3ykm7zmnunxqgpz4mhxue69uhhyetvv9ujuerfw36x7tnsw43qh69dxg

Publishing to

relay.ditto.pub

Author Public Key

npub1hfga8wmley5fzqtttpeupd8hc6s92rykfmzktm8zfdhu9h8exvqsj9ls8k

Show more details

Last Notes

2026-05-04 18:22:04 UTC

I find it such a weird meme that RSS/Atom is dead. Literally every blogging platform has RSS/Atom support. Not just the "indie" ones, even the big corporate ones, like Substack and Medium. Every mastodon account has a built-in RSS feed. Every Bluesky account has a built-in RSS feed. Almost every major news site has an RSS or Atom feed. WordPress automatically produces RSS feeds (and WordPress powers almost half the Web).
RSS and Atom are almost certainly even more ubiquitous than they were in the 2000s, if only because the web has gotten so much bigger than it was back then.
There are more podcasts now than there ever have been, and each of these has an RSS feed.
Every fucking YouTube channel has an RSS feed. In 2005 there were probably fewer than 20 million blogs. Right now there are more than a hundred million YouTube channels.
RSS/Atom is bigger than ever.

2026-02-22 17:27:28 UTC

- reply

@nprofile…az86 Ah yeah! I forgot to link it… https://www.forester-notes.org/30FM/atom.xml

2026-02-19 08:02:37 UTC

amazing. There is a really scary lack of technological literacy in Ars Technica’s journalistic staff. The journalist in question separately gave a statement on social media in which he apologized and called it a terrible mistake, but it’s just not the kind of mistake that an ethical journalist can make, nor is it the kind of mistake that someone educated enough on AI to be writing about it in a journalistic setting can make.
#ArseTechnica
https://arstechnica.com/staff/2026/02/editors-note-retraction-of-article-containing-fabricated-quotations/

2026-02-19 07:34:20 UTC

The daily experience of using the internet is now slower than it was in 1999. Loading a typical page takes 7-8 seconds, because of the virus of cloudflare “verifications”.
I have a feeling that the “solution” is going to be facial recognition challenges for nearly every website in the next for years. And I really don’t want to live with in that future.

2026-02-18 10:00:45 UTC

On my way to my last lecture of the academic year!
Teaching the 'pumping lemma' today. By the way, if anyone has an alternative fucking name for this, I will use it.

2026-02-09 21:37:07 UTC

- reply

@nprofile…w55u @nprofile…5zsz @nprofile…mhl2 @nprofile…t6k2 Yeah… I felt like a toy thing can’t scale. It does indeed need to be near the strength of the Big systems, but preferably with some kind of “language levels” or at least some way to control how much trouble the kids can use it to get into…

2026-02-09 21:02:02 UTC

- reply

@nprofile…5zsz @nprofile…mhl2 @nprofile…w55u @nprofile…t6k2 We actually used a “teaching prover” at CMU to teach things like logic, cut elimination, etc.

2026-02-09 16:32:55 UTC

- reply

@nprofile…47dl W-types are foundationally extremely weak — they are no stronger than having a natural numbers object, and therefore exist in every non-finitist model of constructive mathematics that anyone would ever consider. That is why constructive type theorists do not have any concerns about W-types.

2026-02-09 15:45:00 UTC

- reply

@nprofile…w55u Another example of a 're-think' that would probably occur as a consequence of using a proof assistant is — the unscoped definition of syntax in IB Semantics and layering of typing derivations on top of raw syntax, etc., is going to be far too bureaucratic in any system. Not because of a limitation of the systems, but because of the fact that it *actually is* bureaucratic.
But if you start pulling this thread, you end up quickly doing things like revealing that type preservation is a stupid non-theorem (it should, and easily can, hold by definition) and that only *progress* is a real theorem of programming languages, which starts to undermine the overall ideology that has emerged around it...
Pulling these threads is good, but we also have to think about whether we may end up unpicking the entire sweater...

2026-02-09 15:39:02 UTC

- reply

@nprofile…9rpf Here: https://www.jonmsterling.com/00JB/
But keep in mind, these are my notes on an existing course rather than my take on the subject. Your own lecture notes are probably a lot better than mine.

2026-02-09 15:38:25 UTC

- reply

@nprofile…w55u @nprofile…t6k2 Marcelo and I keep talking about this... It's a very interesting idea. One challenge is to find a proof assistant that is viable for this kind of thing — meaning, one that is not too powerful (so that it obliterates the thing we are trying to teach), not too speculative in its design (so that one cannot conclude anything about mathematics from the fact that it is proved), not to crufty and difficult to use and/or install, etc.....
I might wish to revisit this question once my own proof assistant is up and running ;-)
In the meanwhile, I have been thinking a lot about how we might rejigger the course so that things are done in a way that is closer to the formal way, which usually is the easier way anyway. For example, discrete maths should probably be inverted so that functions and data types are primitive and relations are defined notions, and encodings of data types as big intersections is ...... simply deleted. etc.

2026-02-09 15:15:03 UTC

- reply

@nprofile…47dl Yeah! Or initial algebras in general.

2026-02-09 12:24:02 UTC

- reply

Proof assistants invert the "abstract" and the "concrete" in my experience. What seems more abstract when working on paper tends to be extremely concrete when working in the proof assistant. This is related to the comment of @nprofile…t6k2 a while back that somehow formal proof is more informal than informal proof... (Hope I'm not getting that wrong)

2026-02-09 12:14:02 UTC

- reply

What functional programming and theorem provers teach us is, it is best to set things up so that the rule induction is closer to a definition than a theorem (so we just work directly with the initial algebra, without constructing it explicitly). And nothing is lost by doing so — except several hours of wasted time going on and on about the heights of things, or the “conclusion” of some rule, etc.

2026-02-09 12:11:28 UTC

- reply

I also feel that all this knowledge is kind of outdated now that you can use a proof assistant or a programming language to get a *direct* “synthetic” notion of derivation tree, for which structural induction is the definitional principle rather than something you prove in some complicated and irrelevant way.

2026-02-09 09:50:01 UTC

And now I switch to teaching regular languages and finite automata for the next five lectures!
Unfortunately it always gives me agita about the utterly bungled way we teach structural induction, rule induction, etc. — a result of the collision of two courses that we have not yet managed to rectify…

2026-02-08 22:01:13 UTC

- reply

@nprofile…l3hr That makes sense… or (god forbid) canonical isomorphism ;-)
But anyway, thanks very much for this post. I have been meaning to find out what was going on with that energy stuff and this is very helpful.

2026-02-08 21:45:58 UTC

- reply

@nprofile…l3hr Interesting! But surely definitional isomorphism just means you have maps back and forth whose round trips are definitionally equal to the identity function?

2026-02-07 12:34:44 UTC

Weeknotes 2026-W06
https://www.jonmsterling.com/2026-W06/
+ Welcome to Raphaël Sterbac!
+ Project Pterodactyl: incremental architecture
+ NewsRadar is now NewsDrawer, and it’s lickable

2026-02-06 18:12:07 UTC

- reply

@nprofile…g0zc @nprofile…jxjq I think the British public has far more appetite for the far right than for boring tories…

2026-02-06 17:53:11 UTC

- reply

@nprofile…g0zc you say this, but Nigel Farage is in Parliament, and he's probably going to be the next PM.

2026-02-06 17:36:04 UTC

- reply

@nprofile…sqfw One thing to add to this is, I believe, there are also constructive versions of Barr's theorem that use syntactic methods like cut elimination.

2026-02-06 15:10:31 UTC

- reply

@nprofile…em2h If you go on there it's really funny. It's a lot of "linkedin" style posting, like
How I became confident, by becoming a Mentor with the University of Cambridge Mentoring Scheme
and responses like
So brave, thank you for sharing this amazing experience !!

2026-02-06 08:19:38 UTC

It is so hard to retain good students… they all go to work for companies that can pay them in one year a decade of junior academic income. I won’t actually claim that industrial employment is more stable than junior academic employment (it used to be, but I think it isn’t anymore) — but when you can make 10X salary, it kind of doesn’t matter.
Each year I have a great student who the goes to work at Jane Street, Meta, or similar. I don’t blame them, that’s almost certainly the correct life decision. I also don’t blame those companies for paying so much. I just wish we could compete in the academy. We are experiencing a serious brain drain…

2026-02-05 17:38:23 UTC

This is why prime filters are a good idea ;-)
Very nice thread btw

2026-02-03 19:06:54 UTC

- reply

@nprofile…q0jd well, that and responding to edits without rechecking everything. Like in incremental computation.

2026-02-03 15:55:33 UTC

- reply

This is very subtle, and I unfortunately need to rewrite everything... LOL

2026-02-03 15:54:46 UTC

OK, I think I've finally figured out (roughly) an architecture that will allow me to incrementalise my proof assistant at declaration-level granularity, and even to have diagnostics remain cached when their absolute position changes.

2026-02-03 11:53:56 UTC

- reply

@nprofile…zalk @nprofile…rxrg Guess we should just start talking about “Sequency thingies that satisfy the frame rule” from now on lmao

2026-02-03 11:52:10 UTC

- reply

@nprofile…zalk @nprofile…rxrg Don’t remind me about “Strong monad? The update modality is strong but who cares??” Iris lmao

2026-02-03 09:48:38 UTC

- reply

@nprofile…lfhd I wrote a PhD thesis about it... https://zenodo.org/records/14210117
The final chapter provides some pointers.
And here is an outdated bibliography of papers coming out of the point of view on Artin glueing in computer science that I introduced: https://www.jonmsterling.com/005T/

2026-02-03 09:35:17 UTC

I was thinking about my “Tait computability / Artin glueing” jihad from the time around my PhD, and unfortunately one of its casualties was the acknowledgement that there is anything in PL semantics that is not a logical relation.
In some sense, my emphasis of logical relations (albeit in a different form) as deeply conventional and conservative. But this is the biggest blind spot for contemporary programming language theory, and I deeply regret playing into it.
Not everything is a logical relation. Not even everything that looks like a logical relation is a logical relation.

2026-02-02 13:55:00 UTC

- reply

@nprofile…em2h So do I but I am talking about e-bikes, which are extremely heavy.

2026-02-02 13:52:50 UTC

If it replaces your car, please ride it on the open road rather than putting me in danger on the cycle path by riding a vehicle that packs 3-5X more force than a normal bike.

2026-02-01 22:01:16 UTC

- reply

@nprofile…az86 this looks super fun…

2026-01-29 09:41:59 UTC

- reply

@nprofile…em2h Putting on my wife’s perspective for a moment, though, I think any restrictions on cars need to come simultaneously with a commitment to reliable and cheap busses. The problem is that at the moment, the busses are so expensive (and getting more so every year) that it is not much cheaper to ride the bus than it is to own and maintain a car. During the rainy and dark season, riding a bike is miserable, and my wife simply won’t do it. We are going to save up for a car because we can’t rely on the bus and because the bus is uneconomically costly.
In this country it seems like there is never any coordination around issues like this, so the stick advances and the carrot always recedes. And the bus costs £1 more per year, forever.

2026-01-29 09:22:20 UTC

- reply

@nprofile…em2h This is extremely true. One thing I hear when I say things like this is "But what about the disabled !!! Ableist !!!"
I am perfectly content to let those people drive. If only those who need it drive, then there would be no traffic problem.

2026-01-29 08:55:34 UTC

- reply

@nprofile…em2h That's a good idea.

2026-01-29 08:47:10 UTC

The most frustrating thing about cycling is being caught behind someone on a flat road who is riding with a low gear and their legs are spinning like turbines but they are moving so slowly that even if I have been coasting for a whole minute, I have to put on my breaks to avoid overtaking them.
These people think, "Just pass me!" — but in most cases it is not safe to pass.
1. On a *road* I can't safely pass because there are cars whose actions I cannot predict.
2. On a cycle path, I can't pass because there is opposing traffic.
My message to people who are riding bicycles is: learn to ride it properly before you get on the road. Riding extremely slowly is not safer — it is more dangerous because it causes other people to do dangerous things.

2026-01-28 10:38:51 UTC

- reply

@nprofile…l3hr I don’t mind you it but as a piece of syntax that will be used a lot, it is too long

2026-01-28 09:41:08 UTC

By the way, I hate the word "coercion" in programming languages and proof assistants.
I think "casting" is a bit closer to something that makes sense to programmers, but that too is a bit jargon-y.

2026-01-28 09:30:02 UTC

- reply

@nprofile…j8gu @nprofile…htrj @nprofile…xdkd @nprofile…t6k2 @nprofile…2p65 one last comment: we can *conservatively* internalize judgemental equality in the style of 2LTT, and this allows us to state theorems that take judgemental equalities as a hypothesis. That is actually very useful, even in UF, because for example you may want to prove a theorem that some construction preserves a computational property — such as the product of split fibrations being split. Thats the kind of thing that can only be checked empirically, or proved as a meta theorem, unless we internalize. I actually have theorems like this in my recent paper on reflexive graph lenses and they are useful; they were the only part I couldn’t formalise in Agda, and it is valuable to view these statements as internal ones rather than external ones, because external statements only apply globally and aren’t automatically stable under change of base. So careful internalization of judgemental equality can be useful here.
Sorry for all the messages, I think I am done now.

2026-01-28 09:24:40 UTC

- reply

@nprofile…j8gu @nprofile…htrj @nprofile…xdkd @nprofile…t6k2 @nprofile…2p65 The critique of extensional identity must, then, be that the meta-level notion of equality is unfit for the *intended* purpose, not that it confuses object and meta. It is quite natural for meta things to be internalized (that is what representability means!). In this case the question is merely whether that particular meta thing was valuable to internalize: from my other comment, we see that it is very destructive to internalize it.
In a higher dimensional version of the syntax of HoTT/UF, equality reflection would actually hold for the intensional identity type, and that would be a good thing rather than a bad thing: that the doctrine of \infty-type theories can internalize (proof relevant) judgemental equality as a type without causing degeneration would reflect that the chosen meta-level is a better fit for the intended use of the theory.

2026-01-28 09:24:29 UTC

- reply

@nprofile…j8gu @nprofile…htrj @nprofile…xdkd @nprofile…t6k2 @nprofile…2p65 To elaborate on this, I was thinking about Martin’s comments, and I think there may be some miscommunication about what people mean by “internalising judgemental structure”. If you interpret this in a way that includes everything type theorists mean by it, it must mean nothing more than “is equipped with a salient universal property in the syntactic category” (allowing of course for appropriate variations on what we mean by syntactic category). It is about representabiltiy, like @nprofile…xdkd
says.
That is why the intensional identity type doesn’t internalize judgemental structure but the extensional one does: the universal property of the former does not emerge in the syntactic category but instead in a *higher* category that the syntactic category presents.
The same can be said of sigma types. Regardless of whether they are presented positively or negatively, what actually matters is whether they have their eta law: in the negative case this is the surjective pairing, and in the positive case this is an extensionality law for maps out of the sigma type. In either case, when the law is present, the type former may be said to internalize the judgemental structure of context extension. When the law is not present, they cannot be said to internalize this judgemental structure.

2026-01-28 09:04:27 UTC

- reply

@nprofile…j8gu @nprofile…htrj @nprofile…xdkd @nprofile…t6k2 @nprofile…2p65 Eta is the dividing line…

2026-01-27 23:16:32 UTC

- reply

@nprofile…xdkd @nprofile…t6k2 @nprofile…2p65 Very well put. But let me raise one point that makes me think extensional identity is a different beast.
You can add positive negative product types to a system with positive ones, and it doesn’t change at all the rules satisfied by the positive ones. In particular, adding negative products does not force the positive product to be definitionally isomorphic to the negative one.
With identity types, the situation is different. If you have the “positive” one (the intensional identity type) and the you add the negative one (the extensional one that internalizes judgemental equality), the two become definitionally isomorphic.
I think this is a scientific basis on which to argue that extensional identity is somehow too strong in ways that negative products are not.

2026-01-26 21:56:42 UTC

- reply

My point of view is that generative AI is an interesting and powerful technology that has, due to the need to get a return on investment sooner rather than later, been deployed in harmful and counterproductive ways.
I cannot deny the strength of the technology, but I also cannot accept the breathless pronouncements that all seem to rely on assumptions that are emanating from a managerial stratum that has a lot of money and prestige riding on generative AI "breaking" all systems of production.
I find what some people are able to do using generative AI very interesting and inspiring. For example, @nprofile…d2rh is building Ghostty (a terminal applciation) to an extremely high standard of quality. I cannot take an absolutist point of view on this technology.
On the other hand, this technology is being instrumentalised from a nihilistic point of view to destroy so many vitally important cultural achievements. Both of these things are true, and acknowledging this does not make me a centrist.
I will always fight for technology that empowers people, disempowers the pointy-haired bosses of the world, and brings joy. What our students need is less hype and more 'hard engineering' of all kinds. I am endlessly optimistic about what we can do with the current cohort of students who are in some ways wiser than many of their teachers.

2026-01-26 21:49:12 UTC

One thing I love about being involved in my College is I get a direct line on what young people are thinking.
In my circle of 30-50-somethings, it's taken for granted that "AI" is changing everything. Some of my colleagues express caution that we shouldn't even take any position on software engineering education because it will be out of date within a week.
Meanwhile, my students are telling me that in their cohort, everyone is tired of AI and wants to learn proper software engineering.
One lesson here is: do you remember how clueless your boss was about everything? Recognise when you are in the "boss" demographic, and that your breathless enthusiasm and concern may be equally clueless.

2026-01-26 12:32:33 UTC

@nprofile…prhy By the way, is that bracketing issue with ~Copyable tracked anywhere yet? Let me know if it would help for me to file a ticket.

2026-01-26 10:22:42 UTC

- reply

@nprofile…az86 Yeah... Subtrees are very interesting. Although they have some use-cases in common with submodules, my own use of submodules seems to not really be amenable to subtrees.

2026-01-26 09:58:01 UTC

- reply

@nprofile…az86 I love it... There's some rough edges (e.g. command options that are inconsistent or difficult remember how to use correctly) but it's a huge upgrade over Git for me.
The one part of Git that I use heavily which is not supported is submodules. Jujutsu is so nice that I am even willing to try and find an alternative solution to the problems I am currently solving with submodules.

2026-01-25 22:26:39 UTC

One kind of misleading thing about some explanations of Jujutsu vs. Git is that people say Jujutsu doesn't have a "staging area". This is actually technically true, but as a user of Jujutsu it is probably better to think of
all the mutable (i.e. non-pushed) changes in your working copy
as a hierarchy of named staging areas that you and work on at will, moving things around, etc.
Often the most recent mutable change is unnamed. This one is the "Git-style" staging area, and the named mutable changes are a new kind of staging area that isn't really available in the Git workflow.
I believe this explanation is more faithful to the way that Git users actually use the staging area, vs. systems like SVN where there is nothing of the sort.

2026-01-25 22:21:40 UTC

- reply

@nprofile…r0xq The thing that is helping is basically that Jujutsu provides a local rebase workflow that is more reliable. One way to think about Jujutsu is that whereas Git has one unnamed staging area, Jujutsu has unlimited staging areas that can be stacked on each other in a DAG. Of course, these "staging areas" are just the mutable (i.e. non-pushed) commits in your working copy.
What makes this so nice is that I can reliably edit one of these changes and all the dependent changes get automatically rebased. This is theoretically possible in Git, and I'm fairly good at it, but for some reason in Git it always leads to lots of suffering and cascading failures. One important difference from Git, however, is that the even though the changes have a different commit ID, they keep a separate identity (the "change id") across all edits and rebases.
Anyway, when working on my forest, I sometimes have three or four changes going on at a time. Maybe I'm fixing a certain class of typo across the whole forest; maybe I'm rewriting a theorem; maybe I'm adding a new lecture. Anyway, all these can be done more or less independently, and when one depends on the other, I can safely edit the root without creating lots of unnecessary conflicts. When conflicts do arise, they are easy to resolve as a non-emergency-matter because merge conflicts themselves are a first class part of Jujutsu's change model. I can go work on something else and come back to fix the conflicts, etc.

2026-01-25 22:10:50 UTC

Jujutsu (https://www.jj-vcs.dev/latest/) makes working on my forest so much easier...

2026-01-23 13:47:15 UTC

This website is great: https://www.bugsappleloves.com

2026-01-21 17:31:57 UTC

- reply

Apple can deprecate stuff all they want, won't stop me from writing my own...

2026-01-21 17:30:33 UTC

I'm bringing back the F@#$@#$ NSDrawer!!!
https://media.mathstodon.xyz/media_attachments/files/115/934/271/176/028/522/original/268e0ce9c8810084.mp4

2026-01-21 13:40:37 UTC

There's life before finding out what nickname all your students use to refer to you, and life after finding out what nickname all your students use to refer to you... 💀

2026-01-16 09:23:59 UTC

It can *seem* like it would be better to leave administration to the professionals and spend your time on what you think your job is (research and teaching).
Then just a few years later, you're being forced to use the "Microsoft 365 Copilot App" and all your indispensible internal tools are getting shut down by University Information Services due to actually fabricated security issues...

2026-01-16 09:15:24 UTC

- reply

Don't get me wrong—we still run a lot of things in the Colleges, and there are many things where we can use our bests judgement rather than following lawyer-oriented policies that undermine the function of the University.
But it is a tenuous grasp that is getting slacker every year... That's the reason I've gone so wholeheartedly into all aspects of teaching, direction of studies, tutorial, etc. in my College: I wish to have a firm grasp on these things, preserve institutional abilities and capacity for resistance, etc.

2026-01-16 09:13:00 UTC

Whenever scientists are in control of something, we get lazy and want to hire people to manage it for us.
It is worth comparing the relative situations between Oxford and Cambridge. At Cambridge, the Colleges are weak and not in control of very much anymore, and we are almost entirely at the mercy of University bureaucrats whose interests are not aligned with our own.
I gather the situation in Oxford is very different...
Both are great places, but if ancient institutions have an "enshittification clock", one of them is running faster than the other.

2026-01-16 07:51:52 UTC

It is interesting how good LLMs are at some programming tasks and how absolutely clueless they are at others. This brought to you by trying to get Claude to fix some problems in my tikz code, which was a complete and unmitigated failure 🤣

2026-01-15 17:45:34 UTC

- reply

@nprofile…47dl Yeah… I haven’t read this book but there is definitely a culture in constructive mathematics of doing things very concretely, sometimes in ways that are actually simply incorrect from the abstract point of view. For example, Bishop doesn’t use real numbers at all because he felt that quotients are useless: but then his “reals” don’t have the correct universal property…

2026-01-14 09:06:52 UTC

This week I am seeing a lot of cool recent papers... Is Programming Languages back???

2026-01-13 16:57:31 UTC

I like a paper that has a lot of definitions AND a lot of theorems...

2026-01-13 15:19:15 UTC

I'm having so much fun with synthetic topology right now...

2026-01-13 14:30:16 UTC

- reply

@nprofile…a895 It's basically an entry in a blog or lab notebook — summarising what one did over the week, with special attention to any challenges, etc. I write public weeknotes here: https://www.jonmsterling.com/019X/ (though I've been a bit remiss since the end of the year)

2026-01-13 07:54:59 UTC

One of my students writes such good weeknotes… I love getting these in my newsreader in the morning.

2026-01-13 07:23:42 UTC

- reply

@nprofile…twjf lmao. The type Nat->X is impredicative…

2026-01-12 18:07:44 UTC

- reply

@nprofile…k07g @nprofile…5zsz Love it or hate it, but this is inherited from Smalltalk via Objective-C. The idea is for the method invocation to read like a sentence.
I think Swift’s mix of optional arguments and non-keyword arguments challenges this convention a bit though ;-)

2026-01-11 11:38:47 UTC

My god...
https://media.mathstodon.xyz/media_attachments/files/115/876/266/613/910/477/original/6734f98b334f060f.png

2026-01-10 11:57:44 UTC

I think the reason why constraint-based programming models (including METAPOST but also things like Apple's Auto Layout) tend to be so frustrating is that the coherence of a system of constraints is a global property, which means that when making small changes you must nonetheless understand the entire system.
This means that although constraints themselves are composable in a certain sense (conjunction!), *working systems* of constraints aren't composable.

2026-01-10 11:54:52 UTC

- reply

@nprofile…lrwf The whole idea feels like a late 1980s fever dream (which is exactly what it was). The idea that business people are going to wire up objects in a visual editor to create business applications. There was some really inspiring demos by Steve Jobs in the NeXTSTEP days with this premise... Steve would talk about how the "code you didn't have to write" is best...
I think this was an inspiring and good idea, but what it didn't take into account was change and maintenance: it's indeed simpler to wire up a complex UI once in a visual editor, but when everything is keyed to strings that refactoring tools can't see, there is so much breakage. And that's just in the case where the Interface Builder tool (or subsequent buggier implementations in Xcode) is itself totally bug-free. In practice, it never was bug-free...

2026-01-08 08:57:34 UTC

It is so funny to watch how anyone criticizing any aspect of “AI” who wants to be taken seriously in policy circles always prefaces their comment with the following incantation:
“AI is here to stay, …”
It is hard to understand what they mean by it, but I discovered that if you replace it by the following text, it all starts to make sense:
“In the name of God, the Most Compassionate, the Most Merciful…”

2026-01-08 08:05:17 UTC

- reply

@nprofile…kudx The thing is, I do not want a phone to do internet banking. I do not want to do anything critical on a phone. I am forced to because banks (1) make it take about five minutes to log into their website on desktop each time and log me out after about 2 minutes, whereas the let me work on the phone indefinitely, and (2) banks increasingly gate functionality behind their phone app. All in the name of phony security.

2026-01-08 07:52:18 UTC

The situation for computer freedom is so much better than that of phones.
It’s true that there are no good options for running Linux on a high quality laptop (don’t @ me with options, your favourites objectively suck). But I am happy to give up laptop computing, and there has never been a better time to run Linux on the desktop.
The phone situation is on the other hand horrible. The Android monoculture is so much worse than the iOS one if only because iOS is the operating system of just one vendor, whereas Android and its derivatives are the operating system of literally every other vendor ever. There is no non-Android-derived option, aside from ‘feature phones’ (which honestly sucked back the too).
So why not Android? in a word, it sucks, and it sucks badly. I understand you want to @ me with a bunch of counterexamples and suggestions, but I am telling you to save your breath. As poor as Apple’s taste has been revealed to be in many years, there is still no comparison in terms of polish and reliability, and I believe this goes down to the very foundations of the operating system.
It seems the only real option is to give up phones entirely, but this is rapidly becoming impossible due to the fascist multifactor regime that we are being dragged into (or, which some among us are gleefully cheering ahead).

2026-01-07 20:40:43 UTC

My advice won’t help this person, but this is your reminder: if you are forced to use Microsoft-provided email, be sure to access it using a non-Microsoft email client so that you always have a full backup on your machine.
Thank god the Computer Laboratory makes it easy for us to divest from the University’s idiotic embrace of Microsoft products.

2026-01-07 07:44:52 UTC

- reply

Like, that would be fine I suppose, but if all the references are to events of (1) the 12th Century BCE and (2) the first half of the 20th Century, but there is apparently no knowledge of anything that happened from the year 1964 onward, it just reads like hackwork. Star Trek had the same problem, but the actually made efforts to invent some future-history to refer to.

2026-01-07 07:41:00 UTC

Ursula Le Guin was a great and tasteful author, if only because she does not interrupt her distant-future science fiction to insert some opinion about 20th Century politics (e.g. making some character mention “that ancient conquerer whom our ancestors named The Eysenhoover” or whatever lmao)

2026-01-06 10:00:43 UTC

- reply

@nprofile…rxrg There may be a way to get the internet working, but it's tricky and probably not worth it. I do offline stuff on there only.

2026-01-06 09:45:44 UTC

- reply

@nprofile…rxrg sometimes I still use texlive 2010 for fun…. Maybe I should do that more seriously 🤣🤦‍♂️

2026-01-05 08:27:09 UTC

I love diamond open access journals like LMCS, and others using episciences — which is not only low cost for authors but low cost to run overall.
But as arxiv continues to enshittify itself and simultaneously adopt more extreme moderation practices, it might be a good idea to stop requiring submissions to be on arxiv. We should instead allow *anything* with a DOI, e.g. a paper uploaded to Zenodo.
I currently have a paper submission blocked and overdue because of arxiv’s capricious and meddlesome moderators, who do not understand the publication norms of theoretical computer science.
Arxiv is serving two functions: archival storage with metadata, and community trust. The latter is an important function, but it is not needed for the use-cases of present “arxiv overlay” journals, which need only the archival part. The journals themselves are providing the trust aspect.

2026-01-05 07:06:28 UTC

- reply

One area where consumers can get a variety of high-build-quality appliances is sewing. industrial sewing machines are a different category from home sewing machines, but the differences is not so much a high gulf in build quality, but a difference in functionality. These devices are performing different tasks. But an extremely well-built and repairable entry level sewing machine costing £400 can easily be found.
Contrast with other consumer product areas (like cars!) where the only exemplars built to reasonable engineering standards are antiques.

2026-01-05 07:00:36 UTC

The Juicero story is hilarious and sad for many reasons. There is the obvious reason (that the expensive machine was doing nothing but squeezing expensive bags of juice).
But something that flies under the radar was the extremely, hilariously high build quality of the machine: https://blog.bolt.io/juicero/. It was built like an industrial appliance, but with Apple-aesthetic constraints requiring extremely low tolerances and many custom machined parts. This was criticized (why not make it several hundred dollars cheaper by building to consumer standards) but I think there’s a different, sadder question this raises:
Why is it that consumer appliances are overwhelmingly built to such a low standard, with low grade plastic pieces that chip and snap and shatter when you take them apart, subtly misaligned parts that wear and shear?
It is sad that such so much engineering effort and care was put into a machine that literally has no function, when so little care is put into the appliances that we use everyday.
I know why, but my point is that high quality builds should not be reserved for industry.
Cost is one thing but there are entire product categories where it is impossible to get something that has been carefully engineered.

2026-01-03 09:22:19 UTC

I thought Trump was supposed to put an end to the forever wars… 🤦‍♂️

2025-12-28 10:42:24 UTC

- reply

I am going to experiment with *elaboration* diagnostics (type errors, goals, etc.) not being live / as-you-type. This is in my opinion a huge misfeature of present day IDEs that is more noticeable the more semantic the diagnostics are, and really becomes a usability fault in dependently typed systems.
The simplest idea I have is to elaborate on save. I can even elaborate live in the background but only display it to the user on save. This can make the elaboration feel far faster than it really is.

2025-12-28 10:35:34 UTC

- reply

In my whole career I somehow never needed to attach a debugger to a process that wasn’t started by me IDE… Once I realised how easy this is, my language server development started going much quicker 😂😂😂

2025-12-28 10:29:32 UTC

Got my language server infrastructure working pretty well again, where I can easily emit syntax highlighting information, inlay hints, diagnostics, etc. I am not too long from being able to start wiring up a query-based elaborator — operating directly on lossless concrete syntax trees via a position-aware cursor.

2025-12-28 09:27:35 UTC

It's funny. I've been using Jujutsu for personal projects for a few months and now I can almost barely tolerate using Git.
It is not easy to map the jj <-> git concepts one-to-one. Changes in jj behave kind of like git commits but also kind of like git branches. Technically they are an abstraction over git commits, but when a git user would create a new branch, that is when a jj users would create a new change. But when a git users would create a new commit, a jj user would also create a new change.
In Git it is kind of hard to imagine creating a branch with every commit, but that is because that workflow would become too unwieldy with the need to manually rebase everything and to informally keep track of the intended tree structure of changes. This is handled automatically in jj, which is why the workflow becomes viable.
The jj concept that actually maps onto git branches (bookmarks) is really barely used. I only use bookmarks/branches in order to track and push to remotes.

2025-12-24 15:37:57 UTC

- reply

@nprofile…c9u5 Yes, indeed. My feeling, however, is that 'reference' is very rarely useful. There are systems I'm really deeply familiar with, and even then, I don't really want 'reference' documentation.

2025-12-24 15:08:59 UTC

- reply

@nprofile…p67e Oooo, thanks!! I haven't heard of this one

2025-12-23 12:25:13 UTC

- reply

@nprofile…v38n Very strange. And his relative exponentials are kind of weird because the codomain isn't in the slice. The particular case he studies is very useful in its own right, but it is very strange...

2025-12-23 12:24:14 UTC

- reply

@nprofile…v38n I was reading the part about relative exponentiability.

2025-12-23 12:09:52 UTC

- reply

Someone who .... knows anything at all about presheaves must go through Kerodon like an archeologist, digging for the universal properties that Lurie so “helpfully” unraveled and obscured.

2025-12-23 12:08:58 UTC

God, Kerodon is so nuts and bolts... Even the simplest and most natural definitions are spelled out simplex-by-simplex.
It is so strange to write thousands of pages of mathematics whilst trying to avoid having "knows anything at all about presheaves beyond the definition" as a prerequisite.

2025-12-22 09:16:37 UTC

I can’t tell you how often I hear suggestions that we need to adopt “pink” curriculum in order to repair the gender balance — usually this means curriculum that is “holistic” and treats real-world applications and concrete models rather than abstractions and theories, etc., etc., because (as the story goes) women (as opposed to men) cannot maintain interest in something that devoid of real-world implications and you cannot learn that which does not draw your attention.
Without devaluing teaching that treats applications properly, the research shows how wrong and bigoted this point of view is.
What worked at CMU will not necessarily work everywhere, and different countries and cultures have different challenges with the gender balance. But it is worth having a look at their experience.
I’m tired of seeing “gender balance” deployed as a tactic to tear down Theory (usually with stereotypes about how valuing “hard” science or mathematics is somehow misogynistic), when research and experience suggests the exact opposite. https://idf.social/@djoerd/115762206070948483

2025-12-20 10:12:18 UTC

- reply

But one thing I noticed is that even using --without-K, Agda has some very clever things in its pattern matching engine that I would like to disable for pedagogical purposes.
One of them is that you can match on
p : true = true
with
refl : true = true.
This is convenient when you have an inductively defined set, but for my pedagogical purposes, I had set some exercises in which a correct proof would have needed to appeal directly to the fact that the booleans form a set, rather than this syntactic shortcut.

2025-12-20 10:10:04 UTC

I was marking some work from my HoTT/UF module, and I realised it was easier to type the students’ solutions into Agda than to use my brain to check it...

2025-12-19 21:23:05 UTC

- reply

@nprofile…3zl5 god, every day another reason to hate COFEs…

2025-12-18 14:17:05 UTC

- reply

@nprofile…lp7j I’m interested in this question. One thing I am wondering about (vaguely) is that the state of a control that has many states (seemingly a sum) tends to nonetheless be a product, because you need to remember states that you might switch back to. Does this ring a bell?