In today's news:

(a) I did a lot of boring plumbing that got Idris (n+something) into a state where FOUR cannot be far away
(b) I got blocked by a specialist ukulele shop on Instagram, that I've spent a lot of money with, because I dared to criticise them for using AI for a thing that really didn't need it.

Not sure if I'm prouder of (a) or (b) but I'm going to keep doing (b).

Also in the last half hour I've written a song about (b) because that's what I do now. Honestly it's so much healthier (and exactly as effective) as yelling at clouds.

Also (on last boost) why would I need AI to solve the simple problems anyway? One of the great things about learning to solve hard problems is that you can do the simple things without having to dig out the plagiarising planet burning machine. Just like in the before times when we learned to not have to look up every single thing in a reference book.

I'm not sure why I keep saying these things, because you'll either agree with me or think I'm a Luddite. If it's the latter, please read about the Luddites and learn what they *actually* stood for, though.

"AI will solve the simple problems so humans can focus on the hard ones" is such a ridiculous fail at understanding anything about how humans acquire skills and knowledge.

Humans HAVE TO solve simple problems and then advanced problems in order to learn how to solve the really hard ones. This is not optional.

Good luck solving any difficult problems in the future with a generation of people who spent their entire education typing every problem into a chatbot's prompt box.

A simple post for this week's #throwbackthursday - the custom paint job I gave to the neck of my Guitar Hero controller!

#retrogames #pacman

Thinking remains an option. Controversial... but it might even be a superpower by now.

RE: https://mastodon.social/@DamnInteresting/117390632033247253

I don't know about anyone else but I don't think I care what AI can or can't prove in most cases. What I care about is what humans understand in the process.

Nothing in my daily life changes if the Collatz conjecture is proved or disproved by machine, for example. Many things - I can't possibly know what - could be changed by the human understanding that arises in the process.

Believe in yourselves people, for goodness sake. Humans are amazing. It's time you understood that.

(There's plenty of nuance to this as always but this is the internet so I assume people I don't know will assume the worst. You can all go away. Life's too short.)

I’m on the academic job market this year! I’m especially interested in positions at primarily undergraduate institutions and other teaching-focused faculty roles. (Computer Science, more specifically programming language design). If you know of departments that are hiring or folks I should connect with, I’d love to hear from you!

RE: https://mastodon.social/@nixCraft/117372672187422692

Never felt loss, never suffered pain
Never run for cover when it's felt a drop of rain
Never smelled the flowers growing by the country lane
This one's for us

Never loved another that'll never love it back
Never had an itch that it was desperate to scratch
Never woken up and had a cheeky midnight snack
This one's for us

Never rolled around the floor when overcome by laughs
Never felt the horror when it's uttered something daft
Never had the pride and joy of working at its craft
This one's for us

(As some armchair philosopher once said. Leave the art to the humans please. Even when it's rubbish it's *our* rubbish.)

Meanwhile, I found myself thinking about Observational Type Theory today. About 10 years ago I thought it was about time Idris paid attention to that. And now it's 10 years later. Hmmm.

Anyway. Apparently I'm officially visiting Edinburgh University now, so I'll be dropping in shortly to get my Visitor Card so I can annoy the locals. Might also consider venturing further soon.

(Research leave is my favourite thing ever. I'm starting to remember why I even do this stuff. I should do this more often. If only I was allowed :))

I got so bored of finishing off a parser/pretty printer that I decided to do it in the corner of the pub instead of anywhere sensible.

Results: a) I finished the boring thing so I can move on to the interesting things. Yay!

b) I learned that there is a St Andrews Madrigal Group. They were playing Jenga on a wobbly table, and it was entertaining to witness.

I say "worked at". Technically, the right phrase is probably "been employed by". Don't tell anyone I said that though.

I've only worked at a UK university for 20+ years, so I've only just now discovered that I can get a library card for other university libraries and get borrowing rights and use them as hiding places.

Actually I'm not sure I should give away my hiding places. Still... I can now report that Dundee University library has wifi, excellent sofas, and terrible coffee. And some entertainingly retro CS books.

I went to an open mic tonight because I don't care how embarrassing I am any more. I did my usual nonsense, but also asked who else was a snowflake. They all cheered (they were weirdly attentive for some eejit in a hoodie with a ukulele...).

The avalanche is coming. Keep fighting, and make sure you're having fun on the way. Joy is an act of resistance.

I am VERY PROUD of this joke. I don't care what you think. Leave me alone.

https://types.pl/@edwinb/117356697131505939

Related: I think I stopped enjoying research for a bit because I was trying too hard to please everyone, which is of course impossible. Ricky Nelson teaches us a valuable lesson here.

Also I have just earwormed myself.

I've just seen Someone On The Internet say (in a video so I won't waste anyone else's time...) that "Idris 2 promised to be systems level, and the betrayal is now evident".

I wonder who promised that. I try not to promise anything because I change my mind too often... maybe I handwaved it in a talk at some point or something. Or in a pub. I do that sort of thing at the point in the evening when we move on to "wacky ideas that will never work".

Anyway. For the record, the thing I'm working on now will be whatever I want it to be, and probably not the thing I have in mind now, and if you feel betrayed by that, I'm sure there's other cool things you can use.

On last boost... Last year I had to replace my washing machine and it was next to impossible to get one without wifi, so I gave up and accepted it. Have I ever connected it to my wifi? Of course I haven't.

I mean I'm sure there are more innovative ways of making clothes cleaner that I have never even dreamed of, but I'm pretty sure it's got enough of them in its default set up.

Do not, under any circumstances, connect your appliances to the Internet.

“Owners mourn spoiled food after firmware update bricks Samsung smart fridges”

https://arstechnica.com/gadgets/2026/09/owners-mourn-spoiled-food-after-firmware-update-bricks-samsung-smart-fridges/

I feel like I've made more progress on the new Idris in the last fortnight than in the previous six months. This research leave lark is great. If only I could do that all the time... Just about to get cracking on a new elaborator which for me is the most entertaining part.

On the other hand I have to write a new parser now, which is less fun. Swings and roundabouts...