Jon Sterling
jonmsterling@mathstodon.xyz
<p>I am an Associate Professor in Logical Foundations and Formal Methods at the Cambridge Computer Laboratory, and a Fellow of Clare College.</p><p>I like categories, domains, and vintage computing.</p>
Posts
-
Post #3740452
RE: https://sfba.social/@drahardja/116899003692938721 What I find really frustrating about the present moment is — if you say something like “It is not a good thing for airplanes to be enhanced into birds by cameras”, you get all these people coming out of the woodwork saying things like “Boy, if you think that your phone wasn't changing your picture before AI, you are really mistaken” or something. It's true that cameras do an immense amount of processing of raw data in order to make...
-
Post #3668908
This is really disheartening… https://www.bona-books.com/news/we-bought-an-ai-story I wish this publisher the best in a very difficult moment. I feel sick to my stomach for the genuine short story authors who are nowadays at risk of being published alongside slop.
-
Post #2705709
RE: https://mastodon.social/@tonofcrates/116601142050958775 I remember recently I saw some established academics saying things like, the LLMs can/will write better papers and reviews than us anyway. I remember thinking, “Speak for yourself LOL”. These people really are telling on themselves… The entitlement is amazing: somehow they believe simultaneously that society should pay them a full professor&#39;s salary to do something that they are admittedly terrible at. Call me crazy, but if yo...
-
Post #2649901
Here&#39;s a kind of 101 thing that a lot of people in the world of AI coding are missing, I think. Question: What are the implications of the fact, &quot;All the tests pass?&quot; Answer: It actually depends on how the code was written. Unfortunately, the salience of &quot;all the tests pass&quot; has a lot to do both with the strengths of agentic programming and the weaknesses. If code was written without knowledge of the tests, and then happens to pass the tests, I thin...
-
Post #2649900
I don’t really like property-based testing, insofar as it involves randomized inputs. 1. Randomized tests are inherently flaky. If the code is correct you don’t notice, but if the code has a bug in some edge case, then the tests (by definition) will pass and fail nondeterministically. Flaky tests have just one destination in my judgement: the bin. 2. Picking a realistic input distribution can be as difficult as writing the code you are testing. Sometimes more difficult. It is easy to get fals...
-
Post #2649899
Not to step on a culture war landmine, but I keep seeing people claiming that the reason we know Memnon in Greek mythology was black is that he was portrayed as such on various amphorae. The character of Memnon is indeed African, and he was certainly considered to be black or at least dark-skinned by writers in antiquity. That much is true. But the amphora art has nothing to do with it… Almost everyone on there is depicted in black pigment. That was the art style. It&#39;s called black-figu...
-
Post #2649898
I guess it&#39;s old news to complain about how carelessly engineered Apple&#39;s Music.app is, but seriously…
-
Post #2649897
i want to GRILL seitan...
-
Post #2531597
God grant me the boldness of a University that requires faculty to complete &quot;cybersecurity training&quot; whilst also forcing on us the biggest security vulnerability of all: The Microsoft Office 365 Copilot App.
-
Post #2334013
Weeknotes 2026-W19 https://www.jonmsterling.com/2026-W19/ + Algebraic foundations of bidirectional elaboration? + Happy 100th Birthday to David Attenborough! + Reading Corner: Annihilation, Authority (thanks, @nilesjohnson)
-
Post #2334012
After a few hours of reading tormented and writhing student proofs, it is of such immense satisfaction to sit down with a blank sheet of paper and write the proper proof in one go with no mistakes, everything in its right place, scaffolded properly so that it can be read from start to finish.
-
Post #2334006
It’s Seitan-making day. Wife makes the dough, I wash it. I can’t wait to eat it.
-
Post #2202432
RE: https://types.pl/@amy/116522250630340534 Sending my best wishes for the future to the team behind Mikan. I don&#39;t necessarily agree with every single choice made here, but I find that their approach is based on a love for Agda and respect for its users. I am very sad that this kind of quality-control could not be accomplished within the existing Agda community, but I am also very hopeful for the future. I wish nothing but the best for both the Agda developers and the Mikan develop...
-
Post #2202431
I saw a rook today on my way home! First time I’ve ever see one in person. Beautiful birds!
-
Post #2202430
RE: https://mathstodon.xyz/@highergeometer/116526500300835429 Wow! This is right up my street.
-
Post #2202426
Had a read of two of my students&#39; draft theses this week and this stuff is looking really cool… Very proud of my students.
-
Post #2202425
My wife asked me to tweet out the following: “The X-Files is the Law And Order of science fiction”
-
Post #2164922
I am almost afraid to ask, but do people have macros or a package for doing reasonably typeset grammars, of the kind you often see in PL papers? (Please don&#39;t answer this if you don&#39;t have really high standards for typesetting. For example, if you have ever typeset a word in math mode without wrapping it in an appropriate command, you would probably not be in the target audience for this question.)
-
Post #2125752
The reason the Erdős problems are interesting is that he set them with the idea that solving them would require some new understanding, which was the real goal; if it happens that the problem can be solved “simply” by aggregating existing understanding (even in a very sophisticated and expensive way), it indicates only that the setting of the problem failed in its goal. You aren&#39;t going to use the solution to an Erdős problem to suddenly crack the problem of economical nuclear fusion or...
-
Post #2117127
If you&#39;re interested in synthetic topology and synthetic higher category theory, you might like to check out this manuscript that @FredrikBakke, @markwilliams, Lingyuan Ye and I have uploaded to the arXiv: THE SYNTHETIC SIERPIŃSKI CONE https://arxiv.org/abs/2605.00773 There is an interesting story behind this work that I will tell later. ---- In domains, categories, and toposes, the Sierpiński cone construction glues onto a space a universal closed point lying below all the other poi...
-
Post #2076705
We should fork projects more often. I think we worry about fragmentation and about losing momentum, but we should be clear that there&#39;s two kinds of momentum: 1. Community popularity, contributor, and funding momentum. 2. Development/improvement momentum. I think the first one doesn&#39;t really matter. First of all, project popularity is just braindead internet points that you can&#39;t eat. It doesn&#39;t matter. Splitting the contributor base doesn&#39;t matter eit...
-
Post #1969696
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...
-
Post #1938724
Really feeling this: https://blog.feld.me/posts/2026/04/open-source-does-not-imply-open-community/
-
Post #1846848
Weeknotes 2026-W18 https://www.jonmsterling.com/2026-W18/ + An injury healing + Preparing a few manuscripts + Thinking about POSSE + Speaking of Forester… + Reading Corner: Children of Strife, The Doors of Eden
-
Post #1846847
A spine is the best thing in the world to have…
-
Post #1831754
What I try to teach my students is to follow your conscience, and listen to your heart. In life there are many temptations, and professional environments sometimes warp your point of view until you start to think that by following your conscience you are doing wrong rather than doing right, or that you will be left behind if you do not comply. Sometimes the temptation is to “pivot to AI”, or otherwise represent your work as something it isn’t in order to be heard. Sometimes the temptation i...
-
Post #1820390
Nix: not even once.
-
Post #1815120
I increasingly find that mathematics without *either* the axiom of choice *or* the axiom of univalence is very punishing. This may be one way to rationalise the mistaken propaganda of certain people that univalence is about constructivism. It&#39;s obviously not about constructivism, but I think that constructive mathematics is probably not viable without univalence. So it&#39;s a question of who needs whom... The reason is that there are many places where you can do some construction...
-
Post #1802959
Once again, I am getting polynomial functor pilled.
-
Post #1802958
A lesson about Agda and Rocq&#39;s design. When you design a proof assistant entirely based on “I want this exact code to typecheck because I just KNOW it&#39;s fine”, it&#39;s hard to be in control of what *other* code typechecks. Beware.