In , ever wonder what goes in the brackets in `destruct x as [...]` or `intros [...]`? Wonder no more: coq.inria.fr/distrib/V8.8.2/re

It has some neat features if you're into unreadable one-liner tactics (that noone is going to read anyway) like me.

lyxia boosted

Contemporary Canadian illustrator Julia Iredale, known for her depictions of curious surreal scenes and landscapes #womensart t.co/a5G4NQZbgi

In the 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.

lyxia boosted
lyxia boosted
lyxia boosted

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.

lyxia boosted

We wrote an open letter (in French) to protest against France's renewal of their Elsevier subscription for 4 more years:

blog.dissem.in/2019/lettre-ouv

lyxia boosted

My, I like new changelog links on @hackage posts!

Now I want to give every package an ActivityPub outbox and a profile page. And that brings me back to implementing a #Fediverse capable feed server.

lyxia boosted

to formally model "stuff, structure and properties".

math.ucr.edu/home/baez/qg-spri

> 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

lyxia boosted

The "Selfie" attack on TLS 1.3 explained, and why formal verification efforts didn't catch it:

nadim.micro.blog/2019/04/11/se

Heard on IRC:

<Tuplanolla> (...) Haskell, which is basically Diet Coq (...)

lyxia boosted
lyxia boosted
lyxia boosted
lyxia boosted

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.

lyxia boosted
Show more
niu.moe

We are a cute and loving international community O(≧▽≦)O !