Daniel ✨🐚 @daniel@types.pl

putting the final touches on my Lambda Days slides! come along at 3:30pm on Tuesday (or watch the video later!) for a whirlwind tour of linearity, uniqueness, ownership and borrowing, and to find out about a framework of graded types expressive enough to accommodate them all 💙

writing a grant proposal while listening to the ULTRAKILL soundtrack... this is the future of academia 😌​

sharing because this has to be valuable information for at least one person other than me: Fallout New Vegas (including all of the DLC) is available for free on the Epic Games store until June 1st 👀​

does anyone have any (general or specific to PL) standard beginner advice for writing grant proposals? 👀​

(of course I am getting plenty of tips from the person I'm working on the proposal with! but other perspectives are always helpful when you're doing something for the first time...)

yeah, I’m bi! that means I’m into people of any gender, as long as they could destroy me in a fight and also happen to have a single robotic arm 😌

> touch thesis.tex

mostly I am enjoying Mastodon, but I do have a *few* complaints...

for instance: choosing this username here seemed like an amazing idea at the time, but I am now beginning to realise that it was in fact a stupid decision for various reasons, and (by design) there is no way to change these without losing all of your posts 🙃​

if you don't like the decisions that the moderators make here, then you do not have to be here! I am both here and on Twitter. you can also be both here and on Twitter. you can only be on Twitter if you like. there are also many other Mastodon instances available! if Twitter stops functioning or existing for whatever reason, and you feel you have nowhere else to go because you disagree with the rules here, then that is not the problem of the types.pl moderators. that is between you and Elon Musk

personally, I feel more comfortable sharing posts about certain things here than I do on Twitter, even though many of the same people follow me in both places. that is explicitly *because* types.pl has a *good federation policy*, which means that I will not have to interact with terrible people who have terrible opinions. on Twitter, I encounter posts from bigots *every single day*, even though I do not follow any of them; on types.pl, I have *never* encountered a post from a bigot, because those posts are *not welcome here*. I am glad this space exists, and I am very grateful to the moderators for not letting it turn into a second Twitter!

if you do not agree with these policies then possibly this space is not for you either. just because the name of the website is "types.pl" and you are a big fan of types (or Poland) does not mean that this website belongs to you. you are a guest in a space set up by others, and if their decisions do not satisfy you then you are more than welcome to set up your own 😊​

Whew, OOPSLA paper in, time to sleep

broke: I "asked" the "AI" to "prove a theorem"

bespoke: I used a language model to generate a sequence of tokens that would most probably follow the theorem statement and then the word "Proof:" based on its training data, which might more closely approximate something that looks like it could be a proof of my theorem as the model is trained on more data