wen @cyrridven@computerfairi.es
spacemacs is the best editor because it has a secret option to show me a cute text-art kitty on startup
Don't mind me, I'm just learning about the properties of the basic arithmetic units of computers, like, a decade into my career.
(It's actually all bar NaN and -Infinity, but that doesn't sound as neat.)
Floating-point numbers start behaving more and more like Infinity the bigger they get. The bigger x is, the more y there are such that x + y = x. Then x hits Infinity, and we have x + y = x for all bar NaN.
just went to file a GHC bug, only to find that I've been beaten to it by 11 years:
https://gitlab.haskell.org/ghc/ghc/-/issues/3134
in that issue, @simonmar@twitter.com mentions recalling a "very old" ticket about this, 11 years ago!!!
anyway, this bug is still in GHC 8.10.1... 😅
welp this sucks, very disappointed in @Neovim@twitter.com :(
RT @RosaCtrl@twitter.com
The worst part is that the patch was originally submitted to @Neovim@twitter.com, the team asked to send it to upstream (something they usually do to avoid diverging too much) but then it was closed following Bram’s decision 😭 First time Neovim’s devs disappoint me https://twitter.com/ibroadfo/status/1298745527484510209
love me some Designated Social Interaction Time #icfp2020
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 😍
Loved @audreyt@twitter.com's keynote at ICFP'20! I'm pretty much sold on Taiwan now, I guess?
society
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?
mental health
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"
