A handful of you probably know that I've been working with sized types for the past while but probably have no idea what I'm talking about, so I've sort of collected my thoughts on them in a blog post for now: ionathan.ch/2021/08/04/sized-t
This is just one of the problems I've been thinking about, the other being trying to make sure that a sized dependent type system (the one hinted at in the post) without trying to solve anything about an infinite size is at least good and consistent

If you missed my talk about modelling compilation as multi-language semantics, it's now online: youtu.be/RfVhUPkAEKo

I feel the need to write about gender. See profile picture. 

I feel as if I'm being subject to a tyranny of gender. I do not wish to engage in gender. I do not feel attached to gender. But more and more I feel pressured to engage in gender.

I am asked to put pronouns on my bio, and on my name tag at conferences, and to state my pronouns when introducing myself at things.

I do not want pronouns. I do not want to pick pronouns. I go with "he" because it is strictly less complicated, but I'd prefer "they" because it should have less gender, but it doesn't. To say "they" I am engaging in gender. One assumes I am trans, or at least not as I present. Which is probably true, but. What I want is to say "I don't care about gender; I don't like 'he' because it implies gender, and I despise masculinity more than I despite gender. but 'they' implies other thing about gender that I do not care about'.

But that's an awful lot of nuance to impose on a word, and to bring up in every conversation I have with everyone on earth, when I really don't want to think about gender.

Food 

"natural" peanut butter that's just made of peanuts is also more expensive than regular peanut butter that has a bunch of other stuff in it, but this one makes a little more sense, since the little bit of peanuts displaced by the likely much cheaper to produce sugar and oils and gums and whatnot probably do make it cheaper overall

Show thread

Food 

The way things get sugar added to them to replace something else is basically like bread made from flour cut with sawdust

Show thread

“Alright what the hell is this ‘right in front of my salad’ mem… OH”

That's a hamartia (hamartium?) of proof assistants
Either such precision is required that it obscures the spirit of the argument by showing the trees instead of the forest, or you have tactics that solve everything for you to the point that nothing is convincing

Show thread

boost if you have a cat
boost if you want a cat
boost if you are a cat
no one will know which

@systemf @hazel @ionchy Looks like the types.pl mail server needs to have rDNS setup, to avoid some spam heuristics:

```
X-Spam-Flag: YES
X-Spam-Level: *****
X-Spam-Status: Yes, score=5.6 required=5.0 tests=HTML_FONT_LOW_CONTRAST,
HTML_MESSAGE,RCVD_IN_SBL_CSS,RCVD_IN_XBL,RDNS_NONE,SPF_HELO_PASS,
T_REMOTE_IMAGE autolearn=disabled version=3.4.6
X-Spam-Virus: No
X-Spam-Report:
* 0.7 RCVD_IN_XBL RBL: Received via a relay in Spamhaus XBL
* [2600:3c00:0:0:f03c:92ff:fef5:47d5 listed in]
[zen.spamhaus.org]
* 3.6 RCVD_IN_SBL_CSS RBL: Received via a relay in Spamhaus SBL-CSS
* -0.0 SPF_HELO_PASS SPF: HELO matches SPF record
* 0.0 HTML_MESSAGE BODY: HTML included in message
* 0.0 HTML_FONT_LOW_CONTRAST BODY: HTML font color similar or
* identical to background
* 1.3 RDNS_NONE Delivered to internal network by a host with no rDNS
* 0.0 T_REMOTE_IMAGE Message contains an external image
```

Anyway I am like "Proof: By induction over... uh... on... well there's only like five things hanging around so it has to be one of them"

Show thread

@jordyd category theorists will literally reverse an arrow instead of going to therapy

Someone may have suggested this before, so sorry if you're seeing this again!

I want to run a #git "server" on my VPS. As simple to run and use as possible, please.

I want to be able to:

- add it as a remote in my repos
- when I push to it
- it should then push further to two predefined remotes
- should work with any branch at all

#askfedi #help

it's only cyber terrorism when it comes from the russia region of france, otherwise it's just sparkling computer fraud and abuse

oh my gods. they literally have no shame about this.

GitHub Support just straight up confirmed in an email that yes, they used all public GitHub code, for Codex/Copilot regardless of license.

even if NFTs weren't destroying the environment why would you want them anyway

Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.