Jon Sterling

I am an Associate Professor at the Cambridge Computer Laboratory, and a Fellow, Tutor, and Director of Studies at Clare College. Realist of a larger reality.

I like categories, domains, and vintage computing.

Public Key

npub1hfga8wmley5fzqtttpeupd8hc6s92rykfmzktm8zfdhu9h8exvqsj9ls8k

NIP-05 Address

jonmsterling@mathstodon-xyz.mostr.pub

Profile Code

nprofile1qqst55wnhdluj2y3q944su7qknmudgz4pjtya3t9an3ykm7zmnunxqgpz4mhxue69uhhyetvv9ujumt0wd68ytnsw43qdwwmqe

Publishing to

relay.mostr.pub

Author Public Key

npub1hfga8wmley5fzqtttpeupd8hc6s92rykfmzktm8zfdhu9h8exvqsj9ls8k

Show more details

Last Notes

2026-10-21 15:30:16 UTC

Wish I could afford to buy two electronic pages from the ACM... LOL.

2026-10-13 14:12:00 UTC

The transclusion model is great for lecture notes. Sometimes you think that you will never transclude something except once, but it is fantastic to be able to "recall" definitions from earlier lectures.
https://media.mathstodon.xyz/media_attachments/files/117/434/009/732/916/886/original/4b6574a34c8d0d49.jpeg

2026-10-03 12:46:05 UTC

Um, did someone accidentally delete POPL?
https://media.mathstodon.xyz/media_attachments/files/117/377/044/616/601/382/original/63136325cca678ce.jpeg

2026-10-01 07:54:53 UTC

When people talk about how a certain technological advance is “not going away”, I think about all the times that this has actually happened. Civilian supersonic flight is one example that comes to mind.
Pavement that doesn’t crack and crater within fifty (or 500) years might be another example.
These technologies still exist, but they are not widely used. For economic and political reasons.
The same may be true of whatever technology you are trying to force down my throat.

2026-09-29 06:26:57 UTC

I said this to a friend, but it seems relevant here too…
People working on autoformalized proofs of LLM-originated ideas are constantly worried about getting scooped, and I think this might be a little misguided.
This is like me worrying about getting “scooped” to be the first person who read some new book.
I think the “scooping” framing only makes sense for things where you could legitimately hold (or lose) priority on some result, which is just not the case for someone who told the AI, “Find a counterexample for X famous problem” and then mainly contributed by periodically begging it to not stop.
I don’t think this is the end of priority for hand-made results. But we may start to see a two-track system emerge. I know what track I’m going to be on.

2026-09-07 05:13:23 UTC

Looking forward to seeing everyone for Plotkin 80 today in Edinburgh!

2026-08-25 12:52:13 UTC

There's a certain kind of smug asshole whose life changed when they heard of the concept of “revealed preference”, and has never been able to shut up about it since…

2026-08-23 06:21:16 UTC

Another day, another momentary power cut, and several digital clocks with horrible interfaces to set. I hate it!

2026-08-19 09:37:11 UTC

Going to try and get my POPL reserve reviews done today. To those on the PC, so sorry for waiting so long to get started. It's been a hell of a month.

2026-08-18 08:58:16 UTC

- reply

@nprofile…az86 Yeah serious... Actually the reason I have it disabled is very funny. I tried it out and it was surprisingly good for certain things, like figuring something out by looking in my email (e.g. “Who do I have supervising SwSecEng this year??”)
But when you enable it, it replaces the fantastic new Spotlight from Tahoe (the one good thing about Tahoe) with a horrid interface from Hell... So for now, Siri AI stays off.

2026-08-18 07:30:13 UTC

Can I take credit for the restoration of proper window controls after a decade, in light of this radar I filed a week ago? Probably not, but I'm really really glad that the wind is blowing my way again.
https://media.mathstodon.xyz/media_attachments/files/117/115/336/285/346/192/original/3bb157696aa1682e.jpeg

2026-08-16 13:43:42 UTC

- reply

@nprofile…az86 Very nice! I'm extremely excited about embedding the OCaml compiler into the forest! I need to steal this :)
a minor clarification: Graft is not a fork of Forester, but actually a preprocessor whose output is then processed by stock Forester.

2026-07-28 07:56:01 UTC

Amazing. Apple broke the 'NSDocument.isDocumentEdited' state in macOS 27, and they responded to my radar by saying that it is “working as designed”. It is not working as designed!

2026-07-20 08:02:41 UTC

The thing about AI “empowerment” is: a lot of people felt that LLMs would turn the cranks into scientists. What has actually happened is two things:
1. LLMs have turned some scientists into cranks.
2. LLMs have helped some scientists do better work—e.g. I think the Jacobian Conjecture was recently refuted by Claude Fable, which (if true) is a good thing so people don't waste their time on results that assume the conjecture.
I think there are vanishingly few cases where the LLM has empowered non-experts to do *anything*.

2026-07-11 13:13:16 UTC

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 it look like something that resembles our memory of the event. Putting aside the fact that a some of this processing actually is excessive and makes photographs look weird, there's a huge qualitative difference between that kind of processing and something that adds feathers to an airplane or inserts a new picture of the moon.
It's the same as when we talk about generative AI and people say things like "Guess calculators are destroying the brain too huh!!". It's such a Low Brain Energy take.
#nevent1q…64ch

2026-07-03 10:42:27 UTC

- reply

@nprofile…v2v2 Tracking.

2026-06-15 16:04:46 UTC

I am finally delivered from Microsoft Authenticator Hell!!!

2026-06-11 11:17:52 UTC

- reply

@nprofile…az86 Seems still better than the crazy ones of Tahoe...

2026-06-09 13:58:45 UTC

- reply

@nprofile…az86 Godspeed !

2026-06-09 13:10:32 UTC

- reply

@nprofile…az86 They are walking back some of the most destructive changes... Sidebars are back to normal, corner radiuses are still too big but on par with recent pre-Tahoe versions of macOS, menu item icons are removed by default, the tacky 45 degree specular highlights have been removed, and toolbars now have actual bars, and toolbar buttons have some nice shape and give to them. Many steps in the right direction...

2026-06-09 12:36:01 UTC

After messing around a bit with the macOS 27 in a virtual machine, I can really see the potential for professional-friendly software being developed for this UI. It’s not perfect and there are many problems still. But things like clearly separated toolbars, better corner radius, etc. are such a big improvement. I wish we could get full-width toolbars back, though, in the System apps.

2026-05-31 05:40:56 UTC

- reply

@nprofile…snss @nprofile…wu6f I want this.

2026-05-07 17:52:33 UTC

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

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-05-02 14:46:25 UTC

Users of Forester: are you using "objects"?
https://lists.sr.ht/~jonsterling/forester-discuss/%3C5537B252-3A51-40B8-9998-1A3EDD5FE852@jonmsterling.com%3E
Feel free to respond on the mailing list or here if you prefer.

2026-04-07 12:29:44 UTC

WTF: "textunderstandingd" is taking 76GB memory and 99% CPU on macOS right now... god Tahoe is such shit.

2026-04-04 12:26:22 UTC

Tons of work today on Pterodactyl.
I haven't written weeknotes for a few weeks... To be honest, I have felt a bit blocked in the writing department.

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

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"
#nevent1q…swrj

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-20 22:55:04 UTC

I'm thinking about converting opam into my personal mega-monorepo like @nprofile…az86 did… Maybe this can tame the madness...

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:54:22 UTC

- reply

@nprofile…muw6 These things are so baffling and frustrating...
Unfortunately as with most enterprise stuff, the authentication & data protection aspect of things is a huge moat that prevents us from just firing up a 48-hour-hacked replacement that would be functionally far better than the stupid moodle/canvas/blackboard/etc.

2026-02-19 07:39:06 UTC

- reply

@nprofile…4rzu It's really tastefully done.

2026-02-19 07:38:52 UTC

- reply

@nprofile…pw0n I recently learned something(which I unfortunately have now forgotten) in finite model theory that actually REALLY depends on the confused traditional presentation of variables.
If it were not so punishing to work on, there could potentially be some interesting things to do in the area of figuring out wtf those people are doing and finding reasonable reformulations.

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-17 22:26:18 UTC

I am just STARVED of coding. I want to CODE CODE CODE and all I am doing is TEACH TEACH TEACH. I love them both, but I want to code.

2026-02-17 22:24:13 UTC

A very memorable MacFarlane-Grieve Feast at Clare College, just in time for our 700th Anniversary !

2026-02-17 22:23:24 UTC

- reply

@nprofile…sqfw I do something like \put\transclude/expanded{false}
Let me know if this doesn't work, and I'll find the real code for you.

2026-02-17 12:42:12 UTC

@nprofile…xdkd Do you know a bunch about lenses?

2026-02-17 09:46:57 UTC

- reply

@nprofile…p7w0 @nprofile…0htv (I guess they did make some changes in Objective-C, like adding lightweight generics, etc. But it was done in a way to avoid breaking anything. Not usually easy to do that though.)

2026-02-17 09:46:23 UTC

- reply

@nprofile…p7w0 @nprofile…0htv Yeah, the Swift evolution has been very .... aggressive; I pretty much skipped the first decade of Swift and that is probably a good thing for my sanity. And dependency issues are present on all platforms where the culture is to use dependencies...

2026-02-17 09:21:24 UTC

- reply

@nprofile…0htv Meanwhile, I can build and run Objective-C code from 2002 without changes. I'm not kidding...

2026-02-17 09:20:51 UTC

- reply

@nprofile…az86 I've been using OCaml 5.3 for several months, and I have started with a completely fresh .opam months ago, so I'm not sure if I can attribute the problem to this... But it's hard to say. When I get some time (ha!) I will blow away .opam once again and see what happens.
You're right about ppx — this is a big source of breakage.

2026-02-17 09:14:48 UTC

- reply

I believe in the sincere efforts put forward by an overworked team... I also believe in the promise of OCaml and the need for continued industrial and academic support of work on OCaml — both to evolve the language and to harden the toolchain.
The issues I repeatedly face can probably be addressed by various workarounds, discussing on the forum, etc. Maybe my current issue is yet another case of "user error". But it doesn't matter.
I am very busy. I need to invest my extremely limited time and attention in platforms where basic reliability is a high priority. OCaml toolchain's unreliability has been a problem for a number of years, and although numerous improvements to OPAM's functionality have been made (and Dune has brought many of its own improvements), this has not seen the overall papercut to "it's actually working" ratio decrease.
Perhaps OCaml should be thought of as the Arch Linux of programming languages. It's completely enlightened, extensively documented, all errors are user errors, and it is guaranteed that your system will break if you leave it unattended for more than six months.

2026-02-17 09:06:42 UTC

Every time I try to do literally anything with OCaml, I experience a new kind of toolchain broken-ness. It's always hard to say what the source of the problem is, who is to blame... Some weird interaction between my environment, ppx, and the general brokenness of the toolchain... In the end, it doesn't matter who is to blame.
The result is that I personally don't build new projects in OCaml until this changes... Obviously I have a lot of work invested in OCaml and Forester isn't going anywhere.
But I find the current situation so frustrating.

2026-02-17 09:03:35 UTC

Anyone ever seen this? #OCaml
> Error: migration error: module open in types is not supported before OCaml 5.02
I'm using OCaml 5.3 !!

2026-02-15 08:24:40 UTC

No kidding…. https://www.nytimes.com/2026/02/15/opinion/junk-food-picky-eaters.html?unlocked_article_code=1.MVA.iL3t.YvV6wif1FEHG&smid=nytcore-ios-share
The call is coming from inside the house

2026-02-15 08:20:03 UTC

- reply

@nprofile…66hp This \land is your \land…

2026-02-15 08:18:14 UTC

- reply

@nprofile…66hp might steal this…

2026-02-13 13:58:47 UTC

- reply

@nprofile…vl77 Ahahaha good luck...

2026-02-13 13:37:29 UTC

- reply

@nprofile…mlrq @nprofile…l3hr Thanks for the pointer !!!

2026-02-13 12:30:35 UTC

- reply

@nprofile…0htv Yeah, agreed!
Re: Bluesky, I guess I can't use my amazing method of blocking all the crazy people on there because blocks are stored publicly. I mean, it's bad enough that this stuff on Mastodon is visible to admins, but on AT it is a whole nother level...

2026-02-13 12:14:19 UTC

- reply

@nprofile…qsmz (Oh, perhaps it wasn’t clear that this little bar is only used when you have some useful buttons to put down there. Like something to make a new folder. It’s not wasting space: it’s adding affordances to productively employed space.)

2026-02-13 12:11:24 UTC

- reply

@nprofile…qsmz That’s a really weird take…

2026-02-13 10:43:49 UTC

- reply

I love it too, because maybe someone will say I am ableist if I am disproportionately blocking people who behave as though they have an untreated mental illness. And I can just block those people too.

2026-02-13 10:42:48 UTC

The thing that really changed my online life was when I realised that when someone is boosted into my timeline saying things like “If you do/don’t X, you are a eugenicist”, I can just block them. And I will never hear from them again.
When I first realised this, I blocked a lot of people. Now I don’t have to block that many people that often.
Maybe I am creating an echo chamber, but what I think I am doing is limiting my encounters with people behind whom trails a steady stream of trouble.

2026-02-12 18:01:29 UTC

@nprofile…e4nr Wow, I just tried the Bike 2.0 beta and I am so impressed. I had let my license lapse a while back, but I instantly renewed it tonight. thanks!

2026-02-12 12:58:09 UTC

- reply

@nprofile…d423 @nprofile…e93e I have read this, and it's a very cool paper! But it's not about the questions I have in mind.
(Nonetheless, I'm a big fan of this paper.)

2026-02-12 12:23:09 UTC

- reply

@nprofile…ktlj Endorsed.

2026-02-11 15:10:19 UTC

- reply

@nprofile…uhme @nprofile…q0jd Yeah... I get Marcelo's point, but IMO both tree and forest is not a good intuition for what is happening here, so I don't really care too much 😆
And to make it more complicated, if you start with the topos of forests, the actual topos of trees (which is a localisation of the former) is ... equivalent to the topos of forests. It's just that the equivalence does something interesting.

2026-02-11 14:20:28 UTC

- reply

@nprofile…q0jd Yeah... I mean, they both collaborate with each other (and I am personally not really in either half, but on the periphery of one of them).
The two halves are "People for whom it is a great and calming relief to view Iris as taking place in the topos of trees" and "People who get angry and insecure if you mention the topos of trees". Both these groups have produced great work, and their best work has been produced in collaboration. But communication is difficult...

2026-02-11 14:14:30 UTC

- reply

@nprofile…q0jd Another scenario that's always interesting is when there are two schools inventing the same ideas at the same time, sometimes in collaboration but with very different points of view.
Modern program logics like Iris and its community are interesting, because the community cleaves into two halves and there is almost nobody in one half who can even remotely understand the papers of those in the other half, about their own research topic. (With like two or three exceptions — and I am not among them.)

2026-02-11 14:10:28 UTC

- reply

@nprofile…q0jd Yeah… similarly, mathematicians always tell me that reading Gauss is like this too (but I never tried).
I think there are some Greats who were great in ways their peers and immediate successors didn’t understand (leading to things getting worse over time until people go back to the source material) and then there are others whose greatness stemmed from their penchant for deep insights whose importance is understood quickly but whose “ideal form” takes decades and decades to hammer out. And of course many in between.

2026-02-11 14:05:25 UTC

- reply

@nprofile…q0jd it is often so interesting to pull the thread of an idea through history. Often you get to the original paper or papers and it is just unrecognizable or totally garbled. It speaks, I think, to a norm of charity and respect in science.
(sometimes the original is better than anything that came after, but I don’t have a ton of examples of this beyond a couple.)

2026-02-11 12:01:55 UTC

- reply

@nprofile…l3hr Another similar case is Turner’s old proposal of adding a computation rule for funext to ITT, which is totally fine and doesn’t disrupt J. It does disrupt canonicity of course, but that’s a different story.

2026-02-11 12:00:54 UTC

- reply

@nprofile…l3hr I remain convinced that my proposal work modulo the annoying conversion check. The situation is analogous to adding K — which is another universal property but does not have any impact on J.

2026-02-10 21:24:10 UTC

- reply

@nprofile…e4nr I have been really struggling with this. Might steal your design…

2026-02-10 19:34:46 UTC

- reply

@nprofile…e4nr your sidebar is pretty tasteful…

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:13:31 UTC

- reply

@nprofile…xhtk it’s amazing. These people really thought they could get away with anything.

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 21:01:01 UTC

- reply

@nprofile…5zsz @nprofile…mhl2 @nprofile…w55u @nprofile…t6k2 True!

2026-02-09 20:26:10 UTC

- reply

@nprofile…uhme @nprofile…w55u @nprofile…t6k2 And great points about proof as communication, with all the contextuality that entails… I have been drilling this point during my lectures too

2026-02-09 20:25:14 UTC

- reply

@nprofile…uhme @nprofile…w55u @nprofile…t6k2 I think we have an advantage in that we are not training our students to be mathematicians. So we can do things our way without permission :-)

2026-02-09 20:08:02 UTC

- reply

@nprofile…xhtk I really want to do this. And the management is positive about it. I just have to get someone to do it with me 😂

2026-02-09 19:53:34 UTC

- reply

@nprofile…ldyp @nprofile…w55u What I am complaining about is semi-self-inflicted: due to course history I am actually teaching induction like three times 😂😂😂 But to fix this I have to reorganise half the lecture plans and I just haven’t got around to it yet.

2026-02-09 19:52:07 UTC

- reply

@nprofile…w55u @nprofile…ldyp Now I see how this happened …. heh :)
By the way, my students seem to be enjoying your lectures.

2026-02-09 19:01:43 UTC

- reply

@nprofile…t6k2 @nprofile…47dl True! mentioned this later in the thread. There is also apparently a predicative construction that uses bar induction, if that is your speed.
I prefer to work predicatively and take W-types as a primitive.

2026-02-09 18:57:16 UTC

- reply

@nprofile…t6k2 Ahh thanks :)

2026-02-09 17:59:48 UTC

- reply

@nprofile…47dl By the way, there is another constructively interesting proposal due to Bickford and Constable that is predicative but uses a Brouwerian assumption (bar induction). They have a different way to carve out the well-founded part: they look at the part where every path terminates. The hard part is showing that this gives the initial algebra, but if bar induction holds you can do so.
Bar induction is not accepted by most constructive mathematicians, but it holds in many sheaf toposes. If you start in a predicative and constructive background theory (with natural numbers but without general W types), it seems you can construct a sheaf (pre)topos in which bar induction holds, and this pretopos should have W-types.
(Don’t quote me on this, but I believe it will work.)

2026-02-09 17:00:54 UTC

- reply

@nprofile…47dl The constructive way to do it is first define the dual type of nonwellfounded trees and then isolate the wellfounded part. This is very easy. The hard part is to see that this is small. For that you need some kind of impredicativity (as holds in every topos).

2026-02-09 16:55:28 UTC

- reply

@nprofile…47dl there is an impredicative encoding. So predicativists do need to assert them as a basic axiom; predicativists tend to make up for lacking a subobject classifier by taking many very powerful forms of induction as a primitive.
In any case, all these kinds of induction preserve the computational character of the system, which is one dimension of constructivity. The other dimension of constructivity is having sheaf models, which is also trivial.

2026-02-09 16:52:08 UTC

- reply

@nprofile…47dl Well, the proof I gave doesn’t work for all W types haha

2026-02-09 16:35:04 UTC

- reply

@nprofile…47dl Of course, you probably do encounter well-founded things with some frequency in geometry, e.g. Noetherian assumptions, 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 16:31:13 UTC

- reply

@nprofile…w55u We should talk about it. I think that even the unreasonable ones can be dealt with in the way I propose.

2026-02-09 15:48:12 UTC

- reply

@nprofile…9rpf Heh. I want to move more toward implementation-driven because I feel that is where the real mathematics is...

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:24:44 UTC

- reply

It's also a good way to see the importance of one object having more than one universal property. For example, although |->* is the reflexive transitive closure of small steps, in order to prove that small steps imply big steps, you want to use a different universal property (the smallest reflexive-on-values relation that is closed on the left under small steps).

2026-02-09 15:22:24 UTC

Taught my first 1B Semantics supervision of Term — very fun! Supplementing Peter's very effective teaching of rule induction with practice proving things using the universal property of various relations. I like the latter style, because instead of "blah blah blah, by the induction hypothesis, blah blah blah" fuckery, you are just establishing closure conditions.
My style is very sensitive to getting the correct 'induction motive', but that's a good thing because it makes it really easy to see if you are doing a real proof, or just a proof by gesticulation.

2026-02-09 15:15:03 UTC

- reply

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

2026-02-09 13:57:09 UTC

- reply

@nprofile…xwtp @nprofile…4az5 Very nice! Glad someone took this up properly.

2026-02-09 13:49:57 UTC

- reply

@nprofile…pw0n Yes, I want to handle this carefully… this is somehow even more important in HoTT — where we have really tricky path inductions to consider.

2026-02-09 13:10:49 UTC

- reply

@nprofile…2p65 so weird and unnecessary…

2026-02-09 13:07:29 UTC

- reply

@nprofile…pw0n Yes… This is really important.

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.