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
Edwin Brady
boosted
Hey people: please, when you use agda--categories, don't just link to it, cite the paper! Proper academic credit is important, and citations are the way you do it. Maybe in the future, links to github repos will count as citations, but right now they don't.
I've see two recent papers on the arxiv which could be thus 'augmented'. I won't @ the authors (yet?)
Nearly back to Scotland. I got slightly held up in Newcastle because a former member of Lindisfarne was doing a gig in the station pub, and I am old enough that I don't care about admitting that I stayed to listen :).
On the train south, since today I'll be visiting the town where I was born. I can't remember when I was last there. Decades ago, most likely...
My mp3 player has just randomly picked "Going Home" by Mark Knopfler.
Coincidence is entertainingly weird sometimes.
*digs air saxophone out of bag*
I'm speaking at a conference next month. It's been a while. What happens?
Anyway, I see lots of my internet friends will be there too. I'm looking forward to venturing out further than I've been for a long time!
https://www.causalislands.com/sessions/idris-2-quantitative-types-in-action
We have a week off teaching so I get to do some research and some hacking on Idris. So far this week I've done exactly one thing, which is changing a "True" to a "False".
It only took three days to work that out...
(Next step, change the Boolean to something informative. Might be done by next Christmas.)
Edwin Brady
boosted
Oh dear, I managed to get all of two points, but only because I had better taste in email/social media services ...
Edwin Brady
boosted
Hello, world! We are the Programming Languages group at TU Delft. Our current members on Mastodon are @casperbp, @dennis, @virtlink, @liesnikov, @baboum, @casvdrest, @pdmosses, and @agdakx. Stay tuned to this channel to hear all the latest updates from Delft about #Spoofax, #Agda, #TypeTheory, #ModularLanguages, #WeakMemoryModels, and #ProgrammingLanguages in general. #introduction
Edwin Brady
boosted
Here it is, the Top40 from 40 years ago today! Rammed with bangers!! Also the album charts (on certain transmitters only) (1983)
Now imagining that the questions in the Voight-Kampff test are "Are you a robot?" then "Please point at the traffic lights".
A captcha just asked me to identify the traffic lights to prove I'm not a robot, and suddenly I'm worried about self driving cars.
(Well I was anyway, but still...)
Edwin Brady
boosted
i just realized that there is an entire generation of e-mail users who use the word "CC" and have no idea what it means.
Carbon Copy was a process used to make identical copies of writing (or typewriting) through one or more pieces of paper. it involved using a sheet of thin carbon paper in between two pieces of paper - as you wrote/typed on the top sheet, the carbon would imprint on the bottom sheet using pencil/pen pressure alone.
in the below image, the yellow sheet is the top sheet that you write on - there is a black sheet of carbon paper beneath it - and then a pink sheet that receives the copy below it. the customer gets the yellow sheet, the restaurant keeps the pink sheet.
ChatGPT just asked me to verify that I'm human, and I'm not sure what to think about that.
Edwin Brady
boosted
Regretfully, the petition to remove #LGBT content from the #UK curriculum has 197,100 signatures.
The counter petition asking for that content to remain, is rapidly gaining ground. It now has 78,919 signatures!
Pls sign the counter petition if able. British citizens & UK residents have the right to sign. Pls boost otherwise!
Link to official petition to UK Gov & Parliament: Do not remove LGBT content from the Relationships Education curriculum
Edwin Brady
boosted
Type-Theory as a Language Workbench (EVCS 2023)
@gallais, @edwinb, and I received the word 'unconditionalised' yesterday.
Our paper, submitted to Eelco Visser Commemorative Symposium was fully accepted.
Sad, but happy.
A link to the github (containing source + paper) is available:
https://github.com/jfdm/velo-lang
ArXiV version coming soon.
DOI'd artifact is https://doi.org/10.5281/zenodo.7573031
The new Idris core has finally successfully compiled some code and so @gallais and I have had a celebratory pint or few. I'd try to check the prelude but I'm too scared tonight... Maybe tomorrow.
Anyway, it's January 25th, so by law I have to go and eat haggis now.
Just went to pick up a ticket to see @brianbilston in a couple of weeks. I'm looking forward to seeing how he maintains his anonymity. I'm imagining a paper bag with eye holes and so I'll be disappointed with anything else.
Edwin Brady
boosted
Where is the AI app that turns an overproduced 10 minute YouTube video answering a simple question back into text that takes 20 seconds to read?
Edwin Brady
boosted
*The C Type System Has Entered the Chat* (one for @edwinb ) https://universeodon.com/@desertfrogger/109657308288525357
- 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
