William J. Bowman @wilbowma@types.pl
- website
- https://www.williamjbowman.com
Paren-wielding meta-theorist. Sith Lord of Compilers.
Joined Oct 2020
William J. Bowman
boosted
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
@ionchy should take a look at page 14 of this https://arxiv.org/abs/2105.06024
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/
William J. Bowman
boosted
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
William J. Bowman
boosted
Food
The way things get sugar added to them to replace something else is basically like bread made from flour cut with sawdust
“Alright what the hell is this ‘right in front of my salad’ mem… OH”
William J. Bowman
boosted
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/
William J. Bowman
boosted
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
```
William J. Bowman
boosted
William J. Bowman
boosted
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"
William J. Bowman
boosted
On why trust in software is at an all time low:
William J. Bowman
boosted
@jordyd category theorists will literally reverse an arrow instead of going to therapy
William J. Bowman
boosted
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
William J. Bowman
boosted
it's only cyber terrorism when it comes from the russia region of france, otherwise it's just sparkling computer fraud and abuse
William J. Bowman
boosted
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.
William J. Bowman
boosted
even if NFTs weren't destroying the environment why would you want them anyway
- website
- https://www.williamjbowman.com
Paren-wielding meta-theorist. Sith Lord of Compilers.
Joined Oct 2020
