← Feed

Posts

• View post

  RE: https://f.duriansoftware.com/@joe/117349807524731580 This is pretty much my story too. But it ended up being so frustrating that I lost interest in programming computers for about five years, until I was able to get my own, which I paid for using money I made from busking on the street as an accordionist. I am not joking.

• View post

  Feeling triumphant. Just made a really good Sichuan stir fried potato….

• View post

  I have a feeling that within a year or so, the venerable agda-unimath library will sadly become filled with slop and slop-derived code. What a shame! I'm hoping that we can get Pterodactyl to the point, within the next two years, that it can support a new iteration of UniMath. I should at some point write something about my suggested guidance on the use of AI in formalisation, but it will be based on the following two principles: 1. We should place no normative constraints whatsoever on wh...

• View post

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

• View post

  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.

• View post

  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's salary to do something that they are admittedly terrible at. Call me crazy, but if yo...

• View post

  Here'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, "All the tests pass?" Answer: It actually depends on how the code was written. Unfortunately, the salience of "all the tests pass" 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...

• View post

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

• View post

  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's called black-figu...

• View post

  I guess it's old news to complain about how carelessly engineered Apple's Music.app is, but seriously…

• View post

  i want to GRILL seitan...

• View post

  God grant me the boldness of a University that requires faculty to complete "cybersecurity training" whilst also forcing on us the biggest security vulnerability of all: The Microsoft Office 365 Copilot App.

• View post

  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)

• View post

  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.

• View post

  It’s Seitan-making day. Wife makes the dough, I wash it. I can’t wait to eat it.

• View post

  RE: https://types.pl/@amy/116522250630340534 Sending my best wishes for the future to the team behind Mikan. I don'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...

• View post

  I saw a rook today on my way home! First time I’ve ever see one in person. Beautiful birds!

• View post

  RE: https://mathstodon.xyz/@highergeometer/116526500300835429 Wow! This is right up my street.

• View post

  Had a read of two of my students' draft theses this week and this stuff is looking really cool… Very proud of my students.

• View post

  My wife asked me to tweet out the following: “The X-Files is the Law And Order of science fiction”

• View post

  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't answer this if you don'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.)

• View post

  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't going to use the solution to an Erdős problem to suddenly crack the problem of economical nuclear fusion or...

• View post

  If you'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...

• View post

  We should fork projects more often. I think we worry about fragmentation and about losing momentum, but we should be clear that there's two kinds of momentum: 1. Community popularity, contributor, and funding momentum. 2. Development/improvement momentum. I think the first one doesn't really matter. First of all, project popularity is just braindead internet points that you can't eat. It doesn't matter. Splitting the contributor base doesn't matter eit...

• View post

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

• View post

  Really feeling this: https://blog.feld.me/posts/2026/04/open-source-does-not-imply-open-community/

• View post

  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

• View post

  A spine is the best thing in the world to have…

• View post

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

• View post

  Nix: not even once.