re: CPP 2021 

This is just a longwinded way of saying tbh

Show thread

This has only happened twice so idk if it counts as a pattern
Pattern matching without K and Definitional Proof-Irrelevance without K
For someone who is on this is ironic

Show thread

Given that it only takes six people tooting a hashtag to get it trending on this tiny instance I'm appalled I haven't managed to get trending yet

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.