#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:
93% of paint splatters are valid Perl programs
https://git-send-email.io/ is live! 🎉
This is an interactive tutorial which will teach you how to use git send-email to contribute to open source projects using git's built-in email tools.