Edwin Brady @edwinb@types.pl
- Pronouns
- He/him
- Shameless promotion
- https://tinyurl.com/TypeDD
Reader in Computer Science at the University of St Andrews. Idris developer, trying to make fancy type systems that are usable and efficient. Occasional Go player. Cricket watcher. Trainee Adult. Will play ukulele for free, will stop for money.
Joined Apr 2022
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...)
Edwin Brady
boosted
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?
Edwin Brady
boosted
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.
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. https://mathstodon.xyz/@christianp/108521945554026396
Edwin Brady
boosted
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.
Edwin Brady
boosted
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.
- Pronouns
- He/him
- Shameless promotion
- https://tinyurl.com/TypeDD
Reader in Computer Science at the University of St Andrews. Idris developer, trying to make fancy type systems that are usable and efficient. Occasional Go player. Cricket watcher. Trainee Adult. Will play ukulele for free, will stop for money.
Joined Apr 2022
