wen @cyrridven@computerfairi.es

going down the floating-point rabbit hole, now considering implementing unums for agda

@edwinbrady@twitter.com anyone tried to do floating-point arithmetic in idris2 yet, or is that position still open?

so far, I've been the first to try and actually use floating-point arithmetic in three different proof assistants

senpai noticed me 😍

I'm also, just, very impressed.

Loved @audreyt@twitter.com's keynote at ICFP'20! I'm pretty much sold on Taiwan now, I guess?

so, can we get publicly archived bodycams for politicians?

So uh, I kinda built a Z3 tactic for Agda today?
https://github.com/wenkokke/schmitty/

my brain, mid-refactoring: hey, you should also refactor that! do it now! you can finish this one later!

me, later: huh, why is my code broken?

I think I'm a little hypomanic at the moment? I'm not sleeping a lot, and I'm working obscene amounts of hours... which, probably not healthy :/

implementing this lattice as an agda datatype... good times, good times...

got an fb recruitment email and I kinda wanna respond with just "😂"

most of my supervision meetings are just my supervisor trying desparately to convince me to do less work, and me going "I respect you, but I'm gonna ignore your advice"

"There have been two key pieces of information used to produce estimated grades: how students have been ranked in ability and how well their school or college has performed in exams in recent years."

so we're just straight up using location as a proxy for race and wealth now?

reminder to always download papers from the author's website! it's probably more up to date and it's free!

updated stack and now my rts is all outta symbols it seems

tbf the fact that there's ads on public transport is kinda dystopian enough in and of itself

every other ad in the bus: "please, please, wear a mask"

danish people: 🤷

guess i'm switching to curl as my main browser from now

if I were a big foundation with a focus on privacy i would simply not potentially discontinue the biggest browser not backed by a company intent on harvesting personal data