C'est assez impressionnant de voir comment la #langue formate parfois ses idées. C'est rare, mais quand ça arrive, c'est assez impressionnant. Il n'y a pas de mot en anglais pour dire « association (loi 1905) ». Il y a bien “charity”, “union”, voire “club”, mais ces mots sont très loins de traduire toute la subtilité de la notion. Ce mec vient d'utiliser “company” comme traduction… c'est tellement à côté de la plaque que je ne sais pas par où commencer 🤦
Parce que oui, pour une compagnie, ce genre de comportements ne seraient pas acceptables. Sauf que #FramaSoft n'est *pas* une compagnie. Apprenez une autre langue que l'anglais les mecs. (Vous remarquerez, je suis gentil : j'aurais pu dire « apprenez sept langues avant de parler », ça aurait été méchant 😅)
Seems like my main problem with proof assistants is that I have to go down to the elementary expressions (with which programmers deal usually) very often, and there is just too many variables to track / keep in mind.
OTOH, maybe it's just the lack of experience, IDK. And I need to learn "surfing" at high level.
Quite the long answer on rituals to appease the #Coq termination checker...
This year, we published a #formalmethods paper "Engineering with Logic: Rigorous Test-Oracle Specification
and Validation for TCP/IP and the Sockets API" https://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf in the Journal of the ACM! :) https://www.cl.cam.ac.uk/~pes20/rems/ #hol4 #tcpip #network so glad that this is finally out :D (happy to hear your thoughts on that, still working on a TCP/IP stack based on that work)
Building #Coq project with #dune works pretty well already, can’t wait for compositional builds to land. And Proof General needs some rework to use the _build/ directory as far as I can tell. Fair warning: most of the resources you may find on the subject appear to concern the yet to be released Coq 8.10
See an example of a not so simple project here: https://github.com/ANSSI-FR/FreeSpec/pull/29
Every time I see the Hacker Ethic praised without critically challenging its shortcomings, I have to think of "Programming is Forgetting: Toward a New Hacker Ethic" by Allison Parrish and wish it was more popular. You can read the transcript here http://opentranscripts.org/transcript/programming-forgetting-new-hacker-ethic/
The final encoding of #haskell freer monads is both faster and more intuitive than the initial encoding. As a ReaderT IO person, I'm convinced final freer is a good alternative for most use cases
Exactly my thoughts on static vs dynamic typing, and much more.
Why does category theory exist?
> When we see enough patterns, we can find patterns in those patterns, and then when we see enough meta-patterns and we find patterns in those patterns, and so on and on until we can't find any more patterns.
#Pijul 0.12 released!
In #Coq, ever wonder what goes in the brackets in `destruct x as [...]` or `intros [...]`? Wonder no more: https://coq.inria.fr/distrib/V8.8.2/refman/proof-engine/tactics.html#coq:tacn.intros
It has some neat features if you're into unreadable one-liner tactics (that noone is going to read anyway) like me.
In the #anime 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.