Pinned toot
Pinned toot

My girlfriend, reviewing my state of the art chapter: Wait, what is a monad?

It feels good writing fiction again. But I have less time to write code and talk about it here x).

lthms boosted

You are PhD student stuck with your family in war zone, and you professor just bring a group of mercenary to rescue you because you haven't finished your thesis yet.

My TypeMatrix is pretty tired, but if I remember correctly it is only 2 years old. :\

Repositories’ size remains bit of a problem unfortunately.

performance has become much better since Pierre-Étienne has implemented new diff algorithm!

I just wait for christmas to pass, then I think I will subscribe to a payed plan to sr.ht. I trust @sir@cmpwn.com to turn an already exiting platform into a very great thing.

Edwin Brady - Idris 2: Type-driven development of Idris | Code Mesh LDN 18
youtube.com/watch?v=mOtKD7ml0N

I am so hyped *_*

I started to read “From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server”[1] (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

[1] arxiv.org/pdf/1811.11911.pdf

Category theory is a good source of exercises to practice 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 (gist.github.com/lthms/61dfad74).

That being said, I have no idea how to prove monomorphisms are injective functions in the Set category.

lthms boosted

Vous voulez développer un machin #ActivityPub mais vous y comprenez rien du tout ? Je vous conseille la lecture de 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 😘

J’ai vu des gens faire le challenge  ; pour ceux qui veulent un retour d’expérience d’une Youtubeuse cool, hésitez pas à aller faire un tour chez Redily :

youtube.com/watch?v=zKClEwgzy7

lthms boosted
lthms boosted
lthms boosted
lthms boosted
lthms boosted
lthms boosted

Haha, holy shit, this is one hell of a meltdown: 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.

lthms boosted

Write.as is now #FOSS! 🎉 We've named the software behind it #WriteFreely.

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: pencil.writefree.ly

Get started with hosting or find a permanent instance here: writefreely.org

Show more
Mastodon

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!