lthms @lthms@mastodon.social

I am no longer a PhD student :)

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).

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

Repositories’ size remains bit of a problem unfortunately.

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

It is almost done :)

https://github.com/ANSSI-FR/FreeSpec/commit/33d636e8afed08e20e3be577c93dedf17cdda188

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
https://www.youtube.com/watch?v=mOtKD7ml0NU

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] https://arxiv.org/pdf/1811.11911.pdf

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.

Coming back to work today \o/.

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

https://www.youtube.com/watch?v=zKClEwgzy7k

#mastoart