you know that "xn--" prefix for internationalised domain names?
til that the "n" was picked at random by feeding some stock market numbers into a hash function
The Multiverse: Logical Modularity for Proof Assistants
#coq blog post: The pro-PER meaning of "proper"
"Dating a mathematical concept is almost always a challenge"
❤️❤️❤️ but it's so worth it.
Blogpost, on proving lists infinite in #Coq
I wrote about a proof by parametricity in Coq
Writing tools I learned from The Economist