Nice article about #Framasoft, they are doing really great things! It also contain quite some background information, e.g. I didn't know that originally Framasoft was a initiative by teachers to share #FreeSoftware with their friends and colleagues. https://www.konradlischka.info/2017/02/blog/how-a-french-association-with-6-employees-offers-mainstream-users-free-and-libre-alternatives-to-facebook-groups-slack-skype-and-the-like/
If you have a #Coq project, you can see its dependency graph in two commands:
coqdep -dumpgraph deps.dot `cat _CoqProject`
dot deps.dot -Tjpg -odeps.jpg
If your modules are nested in multiple subdirectories, sed can also be useful to postprocess deps.dot a bit in the middle. The #unix philosophy in action.
@grainloom @drwho The problem with trying to create a dependently typed systems programming language is that you'd need a model of the whole system's behavior, which is a massive undertaking. The system itself would also need to be well-behaved, which they're not. Program extraction lets you focus on modeling just the properties of the system that you care about.
It would be good to have libraries to make this sort of thing easier.
Fixing OCaml's object system https://github.com/ocaml/ocaml/pull/8562
fediverse meta, on growth and signups
i've said this in replies to people but never on its own, so here it is:
rethink the assumption that open, unmoderated signups should be the norm.
open signups are a tool for growth. capitalist platforms adopt open signups because they prioritize growth above all else. if you value fostering a healthy community, you *cannot* have 100% unmoderated signups. closed networks can control registrations by banning clients once. an open network cannot do this.
Humans are born to be artists, scientists, artisans, and philosophers. Children love nothing more than creative expression, learning to understand things, making things with their hands, and asking deep questions.
But society teaches us not to do these things, training us instead to be “productive”. We’re sculpted to fit into a world obsessed with jobs, money, and ownership, and we’re forced to give up the most important parts of ourselves in order to do so – our creativity, and our curiosity.
Higher-rank types in Standard Haskell
Oh my god, this made my evening
Breaking news in the algorithmic/arithmetic world!
Integer multiplication in time O(n · log n). 
It means you can multiply two n-bits integer using roughly n log n operations. It's a *very* important problem because a lot of mathematical software rely on efficient integer multiplication.
It breaks the last best known algorithm  (Schönhage–Strassen), that was in O(n · log n · log log n)
The C Programming Language, by H. P. Lovecraft:
“Keener news-followers, however, wondered at the events of the winter of 1927-28, the abnormally large number of calls placed upon the stack, the swiftness with which that list was sorted, the disturbing lack of heap allocation throughout the proceedings, and the secrecy surrounding the affair.”
It's hilarious to see Marisa Kirisame (a character from Touhou) on a research paper!