Exactly my thoughts on static vs dynamic typing, and much more.
Why does category theory exist?
> When we see enough patterns, we can find patterns in those patterns, and then when we see enough meta-patterns and we find patterns in those patterns, and so on and on until we can't find any more patterns.
#Pijul 0.12 released!
In #Coq, ever wonder what goes in the brackets in `destruct x as [...]` or `intros [...]`? Wonder no more: https://coq.inria.fr/distrib/V8.8.2/refman/proof-engine/tactics.html#coq:tacn.intros
It has some neat features if you're into unreadable one-liner tactics (that noone is going to read anyway) like me.
In the #anime Space Dandy there are "book-type aliens", which are not sentient nor moving on their own, but are parasites which manipulate other beings to think and move for them. They feed themselves by filling their pages with information. So, books.
This is beautiful and I've never thought about this before:
the convention we have in Unix to pass pre-opened stdin/stdout/stderr fds is not just a nice way to tell the program where to read its input from and output its result/logs to; it is exactly how capability passing should work in a capability-based system. This also is another reason why accepting an -o option (for "output file") is a bad idea.
We wrote an open letter (in French) to protest against France's renewal of their Elsevier subscription for 4 more years:
#CategoryTheory to formally model "stuff, structure and properties".
> given groupoids c,d and a functor u:c->d, the objects of c can
be thought of via the forgetful functor u as objects of d with
an extra _property_ iff u is full and faithful, as objects of d
with extra _structure_ iff u is faithful, and as objects of d
with extra _stuff_ regardless. -- James Dolan
The "Selfie" attack on TLS 1.3 explained, and why formal verification efforts didn't catch it: