#pijul performance has become much better since Pierre-Étienne has implemented new diff algorithm!
Edwin Brady - Idris 2: Type-driven development of Idris | Code Mesh LDN 18
I am so hyped *_*
I started to read “From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server” (DeepSpec project, with @lyxia as one of the author, if I am not mistaken).
Their definition of the itree monad is pretty neat, and it made me realize I don’t need the Bind constructor of the Program monad. It is easy to remove it, and it looks like Coq evaluation mechanisms works well with a bind function for a Program inductive type with only Ret and Request
Category theory is a good source of exercises to practice #Coq modeling. In particular, it really highlights the usefulness of the `Program` keyword to work with subsets.
I have updated my gist, and it becomes really obvious with for instance the Mon category (https://gist.github.com/lthms/61dfad7486364687030984a5ff7f4b40#file-category-v-L164-L275).
That being said, I have no idea how to prove monomorphisms are injective functions in the Set category.
Vous voulez développer un machin #ActivityPub mais vous y comprenez rien du tout ? Je vous conseille la lecture de https://frama.link/ActivityPubTech, c'est bien didactique et on comprend plein de trucs ! Ça manque un peu d'infos sur les signatures HTTP, mais à part ça, y a tout ce qu'il faut pour commencer à se lancer dans l'aventure ! (pis on peut pas lui en vouloir, c'est pas vraiment le sujet du papier)
C'est fait par @starfish et c'est top ! Merci à toi, Narf 😘
A new alternatieve to GitHub etc, licensed under the AGPL 😀: https://drewdevault.com/2018/11/15/sr.ht-general-availability.html
Haha, holy shit, this is one hell of a meltdown: http://ace2018.info/
The summary: it's an academic conference. They invited Steve Bannon to speak. The vast majority of their contributors said "wait, if he's going to be there I don't want anything to do with it" and withdrew. The organizers FREAKED THE FUCK OUT and decided that there was some organized movement dedicated to shutting them down.
WriteFreely lets you self-host a single federated blog or a community of blogs. It's written in Go / #golang, it's lightweight, and runs everywhere -- even on a Raspberry Pi! (We tried 😁)
We just launched v0.1 this weekend, and v0.2 is already coming out early this week. You can try a full demo here: https://pencil.writefree.ly
Get started with hosting or find a permanent instance here: https://writefreely.org
Formal methods researcher · FP Enthusiast
Follow friends and discover new ones. Publish anything you want: links, pictures, text, video. This server is run by the main developers of the Mastodon project. Everyone is welcome as long as you follow our code of conduct!