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: https://ionathan.ch/2021/08/04/sized-types.html
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: https://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.
@ionchy btw I was reading this again and it seems relevant https://pigworker.wordpress.com/2015/01/09/universe-hierarchies/
"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
The way things get sugar added to them to replace something else is basically like bread made from flour cut with sawdust
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
A tool to test if you phone has been hit with Pegasus https://techcrunch.com/2021/07/19/toolkit-nso-pegasus-iphone-android/
X-Spam-Status: Yes, score=5.6 required=5.0 tests=HTML_FONT_LOW_CONTRAST,
T_REMOTE_IMAGE autolearn=disabled version=3.4.6
* 0.7 RCVD_IN_XBL RBL: Received via a relay in Spamhaus XBL
* [2600:3c00:0:0:f03c:92ff:fef5:47d5 listed in]
* 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"
On why trust in software is at an all time low:
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
Paren-wielding meta-theorist. Sith Lord of Compilers.
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.