Jon Sterling

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

I like categories, domains, and vintage computing.

Web site: http://www.jonmsterling.com
Departmental page: https://www.cst.cam.ac.uk/people/js2878
College page: https://www.clare.cam.ac.uk/about/people/master-and-fellowship/governing-body-fellows/jonathan-sterling

Public Key

npub1tr9h95xhp0y87rta506s8284l2jrpvtck5ktd2r3kdph3p7cejqqryhca0

NIP-05 Address

jonmsterling_at_mathstodon.xyz@momostr.pink

Profile Code

nprofile1qqs93jmj6rtshjrlp4768agr4r6l4fpsk9ut2t9k4pcmxsmcslvveqqpp4mhxue69uhhjctzw5hx6egpz3mhxue69uhhyetvv9ujuerpd46hxtnfdu5yaej9

Publishing to

yabu.me

relay.damus.io

nos.lol

Author Public Key

npub1tr9h95xhp0y87rta506s8284l2jrpvtck5ktd2r3kdph3p7cejqqryhca0

Show more details

Last Notes

2026-03-19 07:08:29 UTC

I have a problem with moves to add "AI disclosure declarations" to various things. For code and pull requests, it makes sense to disclose what parts of it were written by AI etc., if AI contributions are allowed by the maintainers.
On the other hand, we have university policies requiring students to "disclose" that their essay is written by AI, and scientific bodies like ACM have policies in place requiring disclosure that papers are in part written by AI.
The thing is, in these latter cases, two things are true:
1) It is actually not acceptable, in the domain, for *any part* of the work to be written by AI. Full stop. I DO NOT WANT TO READ SLOP. I DON'T CARE IF IT IS DISCLOSED AS SLOP. WE MUST NOT PUBLISH SLOP, EVEN WITH A DISCLAIMER. So a disclosure of that kind ought to mean a desk-rejection. It's like the police saying it's required to disclose that you've broken the law: idiotic.
2) Other uses of AI, including idea generation, rubber ducking, "search", etc., should not require "disclosure" any more than using Google or talking to a friend should. I don't "disclose" that I googled something, or that I went to the library and looked at some books. I do cite the things that I use, within appropriate scientific standards, but that's different than citing the tools I used in the course of thinking about things.
So for these reasons, I find the current thrust toward AI disclosure to be deeply misaligned with reality and scientific values.

2026-03-09 09:04:50 UTC

- reply

my advice to students is usually something like: the trend is short, your life is long. research what you are interested in, and make sure you can explain why you are doing it to other researchers (and to beancounters when necessary).
this is especially important for phd students: if you do a "trend project" for your phd, it will be both out of date and "cringe" by the time you hit the job market.

2026-03-09 08:47:27 UTC

RE: https://mas.to/@SmudgeTheInsultCat/116180303224845767
i'm still thinking about academics I know who tried to defend the idea of pivoting to *research* NFTs to me...
i was like "oh wow, ok sure"
#note1g4q…8uad

2026-02-08 09:07:03 UTC

Hylo looks like a very interesting language... Anyone looked at it? https://hylo-lang.org

2026-02-01 19:36:46 UTC

- reply

looks cool… what editor is this?

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 people 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 misinformed.

2025-11-07 07:56:02 UTC

it is so interesting seeing the UK flailing to "capture the magic" of American science and technology innovation. the magic is very simple: 2x-5x compensation.
no amount of "schemes" will make the UK a scientific powerhouse unless one of those schemes involves multiplying all the pay scales by at least 2.

2025-10-30 15:14:49 UTC

- reply

The other thing to remember is that everything is written at a particular point in time in the midst of a particular community discourse & conversation. When you find two apparently incompatible viewpoints represented in two "canonical" papers (even by the same person), this is not a contradiction. Time passes, people learn, the questions they are trying to answer change. Context matters.

2025-10-30 15:13:14 UTC

There's something that didn't really crystallise for me for a long time, which I think I might have learned from Bob Harper implicitly, not sure.
If you like someone's research and want to emulate it, it is more important to read the things that they had *read* than to read the things that they had *written*.
Obviously you should read it all, but I often run into people who are banging their heads against something I wrote when I was just a beginner in a topic trying to understand it myself, and they would be a lot better off reading whatever I had been reading at the time. (A good way to figure out what someone had been reading is to look at the bibliography in their paper or note!)

2025-10-26 11:50:04 UTC

- reply

What a stifling environment, in which even practical research/applied research must always assume some connection with AI. It is taken for granted that “AI has transformed [insert discipline] to be unrecognisable", and all the research proposals have to be about grappling with this “transformation” that has, in most cases that I can see, been mostly fictional or aspirational.
The transformation has not been in the discipline, but in the funding of the discipline.

2025-10-26 11:43:10 UTC

I think the coming years are going to be a bitter reality check for the trend-followers among us — especially those who blew up their entire research programs to get involved in the waning end of an AI boom.
The damage to Universities caused by the top-down “AI / Data Science Only” strategy, which has seen the evisceration of mathematics, fundamental science. and the Humanities, may be irreversible in the foreseeable funding climate. What takes decades to put together can be dismantled in a matter of a couple years.

2025-10-01 17:21:27 UTC

- reply

Personally I feel that is like using Google, or having a chat with your friend. Neither of those activities ever required a "disclosure", so I think that these LLM rubberduck sessions should remain part of one's private thinking process, inalienable by the onslaught of "disclosure requirements" that we are seeing.

2025-10-01 17:07:26 UTC

Please teach your students not to do this.
I understand there is a continuum between spellcheck/grammar check and LLMs, and there could be ways to use LLMs to improve wording or grammar, etc.
But please teach your students not to use LLMs to “draft content”. I don't care if they disclose it (tbh, I prefer they don't!). I don't care if they "take responsibility for the content".
The thing about writing is that it has a social function. The social function is *not* to cause text to exist. The social function is to communicate from your mind to my mind. Text is the means, not the end. If you must use an LLM, skip it and just send me the prompt.
(No, I'm not going to link to the paper. The point is not to dunk on people who end up on the wrong side of a social question. The point is to do better.)
https://media.mathstodon.xyz/media_attachments/files/115/299/998/246/664/023/original/721164289c2725b1.png

2025-09-07 19:51:10 UTC

It is kind of funny. After all these years, although the triumphs of types in so many areas are undeniable, I don’t think any functional+type-based approach to GUI programming has ever really been an improvement on mostly-dynamic objects with late binding.
I have tried dozens of different designs and libraries and languages. Some professionally, some for fun. They are all great in certain restricted ways, but none has felt general-purpose.
I think there is still something missing. I don’t rule out the possibility, of course. It might be that we need more powerful types. But it is also important, I think, to acknowledge the failure of fancy typed FP to deliver what I would consider an adequate answer to the question of general purpose GUI programming. What it has left behind is a wasteland of horrid React apps in TypeScript.

2025-06-16 08:18:05 UTC

I think it's a big success that things like memory safety *have* become legible to the industrial/amateur programming language design community. In part, this is because you can link it to security vulnerabilities and things that actually cost money and may (under certain regulatory regimes) involve at least hypothetical accountability.
What is not legible to industrial/amateur PL designers is the softer stuff — like when type systems make false promises (but the only downside is that the program halts, rather than that it lets you mess with memory in an evil way), or when the compiler can be made to loop on certain inputs, or when you need to break up code into several definitions in order to get the compiler to accept it, etc...
The costs of mistakes like this are not the same as those of memory unsafety, and there is less of a business case for avoiding them. Moreover we are currently seeing a definite trend toward blurring the lines of responsibility and expectations of programming tools.
It's for these reasons that PL designers have a deepened responsibility to "do no harm" — because we will certainly not be prevented from doing harm by business considerations.

2025-06-14 14:02:43 UTC

- reply

You all who are like "Look how careful I am, I remembered to give the case for zero!" are just not teaching with the same level of care as someone who is giving uniform definitions that are simple and work fine and cover every possible case.
A great example is the definition of countable set. Just talk about surjections onto X+1 lmao.
Anyway, I try to do it right in my courses, but the confusion has already set in from high school.

2025-06-14 14:00:20 UTC

I think a big source of people's confusion about zero and the empty set is the following:
(1) Conventional instructors and textbooks are *also* often confused about zero and the empty set.
(2) Even those who are not confused about zero and the empty set tend to treat them as special cases, so rather than giving uniform definitions of things, they uselessly give a piecewise definition with one case for the non-empty and the other case for the empty. If you think of things in such a broken way, it is natural to see the empty cases as mere bookkeeping that is easily forgotten...

2025-06-07 19:21:39 UTC

- reply

I'll let you in on a little secret of structural proof theory that is not taught in enough sources:
Call a rule "invertible" if you can derive the premises from the conclusion. For example, in natural deduction, implication has an invertible intro rule but the elim rule is not invertible. On the other hand, disjunction has an invertible elimination rule but its introduction rules are not invertible.
Anyway, if you are faced with a goal to which any invertible rule applies, you might as well apply it right away as you'll never go wrong by doing so (where "going wrong" means ending up at a dead-end); it doesn't matter in what order you apply the invertible rules. The only thing you have to use your brain for is to decide when to apply *non-invertible* rules.

2025-06-07 19:19:08 UTC

- reply

You started off right. Your goal was an implication, so you applied the introduction rule.
Then your goal was (A => B) |- ((B => C) => (A => C)).
That's another implication, so you might as well apply the introduction rule again.
Now you would have:
(A => B), (B => C) |- A => C
Here you have another implication, so you might as well apply the intro rule once more. Then you'd have:
(A => B), (B => C), A |- C
Now you can start working your way downward with elim rules.

2025-05-28 16:07:57 UTC

- reply

Yeah. And forced to use copilot too if they want to get hired now!
I can't wait for all that to come crashing down.

2025-05-28 15:51:03 UTC

- reply

yeah, tbh it is hard to understand why anyone writing software (aside from people writing corporate Windows-ware) is even on Windows. To get anything done, you need to use WSL, but if you're doing that, why not just use linux?

2025-05-28 11:05:36 UTC

Ghostty is really promising: https://ghostty.org
I still love iTerm2, but I really appreciate that Ghostty is using proper platform-native controls and respecting platform conventions unlike basically any other modernised terminal apps. I also appreciate that it isn't filled with AI cruft.

2025-03-29 10:50:09 UTC

Rewriting the GNU coreutils in Rust sounds fine. Rewriting it with an MIT license? That's giving away the store.
This is one of those times when I think programmers and other technical people need to take stock of the social aspect of what they are doing—which is dismantling a monument to the social ownership and control of software.
Listen, I don't use (GNU/)Linux on my own machines; I use a proprietary operating system because my needs for hardware that doesn't suck completely dwarf all my other computing needs.
But free operating systems are an important part of social infrastructure, and although they have not been able to keep up with hardware advances, they provide an excellent way to *take back* old machines and breathe new life in them, while divesting from the corporate treadmill of "AI", subscription fees, and whatever else.
I think it is far more important that we OWN this infrastructure, bound permanently to the public good, bugs and all. It is a false decision, that we must choose between buggy & insecure software vs. social control of the software. A good-faith coreutils rewrite in Rust would have been GNU licensed.

2025-03-08 22:13:33 UTC

- reply

It is the cost of reproducing the working class :-)

2025-02-10 09:23:50 UTC

This is a fascinating interview of Judith Butler, thanks to @npub1w74…t9ar for posting it.
https://english.elpais.com/culture/2024-12-15/judith-butler-philosopher-if-you-sacrifice-a-minority-like-trans-people-you-are-operating-within-a-fascist-logic.html
https://fedi.ahfrom.synology.me/objects/00cb7174-bd5b-49de-8144-6d3f7dcb45ad

2025-02-04 10:52:42 UTC

- reply

Here is what I am thinking. Dana Scott envisioned synthetic domain theory as a world in which continuity is automatic; on sufficiently nice types, the limits of synthetic omega-chains are actually honest suprema of directed diagrams in the usual sense, but these suprema are absolute in the sense that they are preserved by any function whatsoever.
The way that SDT converts colimits to absolute colimits is as follows: you first take a notion of (co)completeness, like chain completeness or something else, and take the category of spaces that have those colimits and homomorphisms that preserve them; then, taking sheaves on this, you get a new world in which there is a notion of a synthetic category (with the arrows structure coming from the interval) and there is a class of synthetic colimits corresponding to the ones you started with that are now absolute.

2025-02-04 08:53:05 UTC

Synthetic domain theory is a methodology for turning colimits into absolute colimits.

2025-01-31 21:22:12 UTC

this abstract is so absurd. Fuck quanta... I think the Lean team needs to comment publicly to clarify whether they agree with this crap. https://types.pl/@jpoiret/113924659561135969

2025-01-14 07:40:09 UTC

We are so deep into the “AI” bubble now that I had almost forgotten what it felt like when everyone was talking about “blockchain preparedness” and some of our most desperate and opportunistic community members were trying to convince everyone that category theory on the blockchain was the real applied category theory… What a time!

2025-01-11 08:18:34 UTC

Most of the American corporate DEI programs that are being shut down — these were never sincere anyway, I am sorry to say: Meta all but admits that it was just windowdressing. They started when the wind blowed one way, and ended when the wind blew another way. I could be wrong, but I think the main impact will be on the profitability of DEI consultancies going forward.
This is different, by the way, from the changing practices in American university admissions due to the recent ruling, which did have a huge impact on a lot of people’s lives.

2025-01-10 09:22:53 UTC

https://mathstodon.xyz/@danielgratzer/113794833896829163
This reminds me of the time when I bought a bag of doggy treats in Aarhus and started eating them on the street, because I did not see the pawprints all over the packaging (!!!).

2024-12-25 20:30:44 UTC

The recent manuscript on LLMs faking alignment seems really methodologically fishy to me. Part of the problem is that the discourse produced by the LLM about its own “alignment” (a concept that rests on a whole ideology and may be nonsense in the end) is obviously influenced greatly by that of the AI millenarianists, so I am not sure what can really be concluded from the fact that Big Autocomplete has been trained on the sci-fi scenarios that these people like to talk about.

2024-12-22 09:08:27 UTC

- reply

I hope it is clear to people reading this that the pleasant experience of eating chilis is not fully due to “dopamine response” and that people who do enjoy chilis often prefer the flavour of one over that of another. I think, to your point, there is a barrier that you must get past (with computers as well) before you can start to enjoy the wide array of genuine possibilities. This *discerned* enjoyment is not a dopamine illusion — but it may be enabled by it. So I would say any study that concluded “without dopamine, people hated the flavour of chilis” rather than “without dopamine, people were overwhelmed and unable to discern the flavour of chilis” is deeply flawed.

2024-12-17 07:24:41 UTC

The New York Times does not really write articles anymore… They instead write paragraphs all day long and compile them into ever-changing synthetic “articles” whose titles keep shifting (no doubt for “engagement”, as well as tricking me into thinking I haven’t read it yet). These “articles” have no discernible internal structure and leap from one thing to the next.
Imagine spending your whole life dreaming of becoming a journalist at the premier American paper, and then you realise you are just a grunt in the Times’ two-decades-late attempt to catch up to Buzzfeed 🤦‍♂️😵‍💫
The only thing in the Times that actually seems to be intentionally and coherently written is the opinion pages — and one can take only so much of their unholy combination of sanctimonious liberalism and weird catholic conservatism.
No wonder the papers are failing…

2024-12-03 10:38:28 UTC

- reply

I am so tired of all this authentication... I want to stop using a phone, and watch the whole system come crashing down around me...

2024-12-02 07:15:55 UTC

I have to say, I thought the first president to issue a blanket pardon for crimes authorities are not even aware of yet would be Trump, not Biden… 😆

2024-11-28 08:37:25 UTC

- reply

Non rigorous proofs are not at all useful. Approximate answers can be useful, when you can quantify the error — but this kind of quantification is impossible with LLMs. I am sorry to say that in fact, you only *feel* like you have learned more from this than from other methods. If you want to get past zero, you are going to have to start over.

2024-11-27 17:10:53 UTC

- reply

I see so many adults and professionals talking about how they are using LLMs to deepen their understanding of things, but I think this ultimately dives headlong into the “Gell-Mann amnesia” effect — these people think they are learning, but it only feels that way because there are ignorant enough about the topic they're interested in to not detect that they are being fed utter bullshit.
How shall we answer this? I think it speaks most urgently for people who actually know things, those with "intellectual power", to democratise our knowledge, throw aside the totems that make our fields inaccessible and obscure, and open the gates to the multitudes who wish to learn.
At first it seems like it would be easy to compete with LLMs (because they say only bullshit), but to actually compete with LLMs we need to produce educational materials that actually explain things properly. Any 'proof by intimidation' will immediately send our student to the LLM. The moment you rely on something that you haven't explained, same deal. So it may be that this era has a silver lining: we must finally teach mathematics properly.

2024-11-27 16:41:46 UTC

The era of ChatGPT is kind of horrifying for me as an instructor of mathematics... Not because I am worried students will use it to cheat (I don't care! All the worse for them!), but rather because many students may try to use it to *learn*.
For example, imagine that I give a proof in lecture and it is just a bit too breezy for a student (or, similarly, they find such a proof in a textbook). They don't understand it, so they ask ChatGPT to reproduce it for them, and they ask followup questions to the LLM as they go.
I experimented with this today, on a basic result in elementary number theory, and the results were disastrous... ChatGPT sent me on five different wild goose-chases with subtle and plausible-sounding intermediate claims that were just false. Every time I responded with "Hmm, but I don't think it is true that [XXX]", the LLM responded with something like "You are right to point out this error, thank you. It is indeed not true that [XXX], but nonetheless the overall proof strategy remains valid, because we can [...further gish-gallop containing subtle and plausible-sounding claims that happen to be false]."
I know enough to be able to pinpoint these false claims relatively quickly, but my students will probably not. They'll instead see them as valid steps that they can perform in their own proofs.

2024-11-17 13:39:23 UTC

WE MUST FUND INTELLECTUAL INFRASTRUCTURE FOR THE LONG TERM
(a call to action)
http://www.jonmsterling.com/jms-013G.xml

2024-11-06 10:40:07 UTC

Let’s have some good news and cheer today. Mine is that I am enjoying preparing a paper about domain theory for an upcoming conference, and that the writing is not yet feeling like a chore in the way it usually does.

2024-10-28 09:03:09 UTC

Does anyone know of a domain name provider that provides easy-to-access and competent human-based customer service? That used to be Hover, but this is no longer the case.

2024-10-11 11:13:49 UTC

Daniel is being _very_ modest when he says that this is only slightly more algebraic than what people have been settling for: https://mathstodon.xyz/@danielgratzer/113288442719363743. In particular, this article gives a refined notion of "core" that captures or improves upon all the existing examples, has a universal property, and leads to the major CMRA constructions of Iris having universal properties that, moreover, make sense purely at the level of constructive algebra orthogonal to any mention of step-indexing (both analytic and synthetic). Thus these definitions work in *any* model of step-indexing.
I'll be very honest and just say that I have found most of the early literature that explains how Iris is "defined" to be largely incoherent (both in a technical sense and in a scientific sense). Until now, the only answer that has been absolutely reliable has been to look at the Coq code (a deeply unsatisfactory answer, to say the least).
I think that there have been three major milestones in semantically minded people trying to make sense of Iris:
1. Bizjak and Birkedal (2018). On models of higher-order separation logic. https://doi.org/10.1016/j.entcs.2018.03.016
2. Gratzer (2023, PhD thesis). Syntax and Semantics of Modal Type Theory, Chapter 10. http://www.danielgratzer.com/papers/phd-thesis.pdf
3. Gratzer, Møller, and Birkedal (2024, this paper). Idempotent Resources in Separation Logic. https://www.danielgratzer.com/papers/idempotent-resources-in-separation-logic.pdf
With this third paper in my pocket, I am now confident that it is possible to learn Iris without first shutting off your brain. It's great work and well worth a read.

2024-09-30 08:21:09 UTC

- reply

Not sure, I have moved on from such things… Ultimately I found it not as good as I thought.

2024-09-18 13:10:03 UTC

- reply

The other thing is that the most interesting discussions to listen to happen between two or three people who are at relatively the same “level” in terms of expertise and shared context, who *each* have some skill in breaking things down for the audience (who are naturally at a variety of levels).
Back when I worked on a podcast, we tried to interview accomplished scientists about their work and history, but we as hosts were not accomplished scientists and so we could only engage somewhat superficially with our guests. The interview format can work, but it is a lot less interesting and pleasurable to listen to than what I consider the ideal podcast format— a wide-ranging discussion between two people who already have adequate interpersonal rapport and a bit of broadcasting experience.

2024-09-18 13:03:01 UTC

I feel like the big problem with podcasts on technical topics is that most of them have such low production value (*) that they are basically unlistenable. I can take like five minutes and then I have to shut it off.
(* Production value includes not only proper recording equipment and editing, but also things like awkward breathing and pauses, or just the kind of general awkwardness one expects from people without experience in radio — including the weird way that some hosts adopt an uncanny “game show host” or “circus man” persona because they haven’t learned to be themselves.)
Do I recommend starting a technical podcast? Honestly, I would say “No” unless you have certain hard to obtain skills. The results are never as good as you would hope, and I am speaking from experience.

2024-09-02 13:46:37 UTC

Never thought I’d say this, but Cambridge could learn a thing or two from Pittsburgh about road maintenance and transit infrastructure. Look at this pristine busway, which mostly reliably takes you between Pittsburgh and several surrounding villages.
https://media.mathstodon.xyz/media_attachments/files/113/068/264/102/577/234/original/f8aa8c2a61a13eef.jpeg

2024-08-18 11:30:57 UTC

- reply

I have a feeling that a big part of the amazing performance of Apple's laptops, both in terms of battery life and actual "real" speed, is that the software is extremely fine-tuned to a chip that Apple controls. It may be practically impossible to compete at that level for other vendors, but I really hope that improvements in this area can be made.
The funny thing is that Apple's laptop and deskop machines were honestly not very good until you hit the highest end of the price scale, up until the M1 lines came out. Since then, it has been really impossible for competitors to reach even a quarter of overall day-to-day performance for anywhere near the price.

2024-08-18 11:28:24 UTC

I am probably getting to the point where I would consider non-Apple laptops if any of them had even remotely comparable battery life... The Framework laptops are looking really good and I love that you can take them apart easily, but from what I can tell, the battery life is something like 30-50% what one would expect from a low-end Apple laptop. It's kind of hard to imagine going back to that.