Spotted in Newcastle Cathedral earlier today, an Idris logo on a stone outside the crypt.

I'm walking around in varifocals because apparently that's how old I am now. Haven't fallen down the stairs yet. Also it's quite cool that my neck is essentially a manual focus knob.

Nothing quite prepares you for the day the optician first says "varifocals" at you. I'll just be sending my measurements to the undertaker now...

I'm flying for the first time since 2019. Currently at my favourite bit of the whole experience: standing on the stairs so they can create the illusion of boarding even though the plane is nowhere near ready yet.

Remember to credit your sources! Your friends will Judge You if you don't. And so will everyone else, after your 30 seconds of internet fame.

(One of my roles in my day job is Academic Misconduct Officer. I wish I didn't have to remind people of this thing quite as often as I do. But it's important...)

mastodon.social/@glitchritual/

One thing I can say that Twitter’s culture seems to have over Mastodon’s is attribution. On Twitter, you’re likely to get dragged by at least SOMEONE if you don’t properly credit the creator of a comic or artwork or photo you choose to repost; Mastodon users, in my admittedly limited experience to date, seem to give zero fucks. That’s a rare but important strike against this place.

I went to dinner with some family in Edinburgh yesterday. We were early and found an arcade bar to pass the time. This is my new favourite place.

I only got to level 2. I need to go back and practise.

They had some more modern machines too, but who would care about that?

Dependency injection is when I infect your type system with dependent types

Great to hear the late Bernard Cribbins singing the interactive theorem proving song on 6 Music just now.

So that's what I'm doing wrong. Not wearing my lucky hat when I submit papers or grants. To the lucky hat shop!

UK politics. Tories doing what they do. 

It's taken me a surprisingly long time to realise what a perfectly (in)appropriate name Chris Pincher has...

Hmm, I suppose I might know how long my talks took if I didn't allow audience participation. On the other hand, if there's no audience participation, to me there is no talk. I miss an in person audience.

Show thread

I don't think I can remember the last time I got through all my slides. These days I find the most important bit of preparation is knowing all the backup plans and bits I can skip.

But then, I've been giving essentially the same talk since The Day That Time Stopped in 2020 so I'm not sure my advice counts. mathstodon.xyz/@christianp/108

The best thing to do, when you realise you've got 3 minutes and 15 slides left in your talk, is to whizz through them all so quickly that nobody can read anything.

Uh huh.

I am really glad when people add alt text to images on Mastodon.

My internet is so damn slow, that images never really load (i turn them off anyway), but at least I can get a sense of what it is from the text ^____^.

Looking at some old code wondering "Which numpty wrote this?" again.

Past me could have been a bit more helpful to present me. But it's okay, I think future me can deal with it.

This is the most excitement I've had in more than two years. Idris HQ has moved to Duke's Corner.

Show thread
Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.