re: NbE for Sized Dependent Types 

The reason size irrelevance seems like a hack to me is because I can't intuitively tell when I should be using relevant sizes and when I should be using irrelevant ones
Maybe once I understand it'll no longer seem like a hack

Show thread

I made a twitter thread. No idea what kind of magic keyword I put but got some weird robo-likes on it

Do you use a Mac and need plenty of RAM? All new apple chip Macs have a max of 16gb. 😭​

How many toots do I need to become a professional tooter?

I do not like walled gardens. That's why I've joined another one.

Will I just keep asking rhetorical questions and thus begin a new persona in a new social network?

Show thread

What is the etiquette here? What are the expectations?

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