Martin Constantino-Bodin @MartinShadok@aleph.land

@MartinShadok
Looking forward for a paper entitled Subverting Assurance by Live-Patching a Proof Checker's Core…
@lthms

@MartinShadok I really want to understand better how Coq works under the hood in the future.

“Don’t trust your TCB” :D

@MartinShadok
Is there a place for "super-optimization" in #Coq?
@axiom

@MartinShadok I consider a proof incomplete if it's not automated ;)

D'où cette unpopular opinion : la gauche n'a jamais été aussi faible que depuis l'avènement d'une époque où la minorité politisée croit que le summum de l'action politique, c'est de n'être dans aucun parti parce qu'ils ne leur pardonnent pas d'être imparfaits.

En vrai je me demande comment ça se passe dans la tête de @manuelvalls@twitter.com qui a passé des années à se branler sur le fait qu'il était "républicain" et qui va maintenant faire campagne pour que la Catalogne soit pas une république et reste dans le giron d'une monarchie

@MartinShadok I just remembered, in the same lecture there actually was a demonstration of why Coq itself would be inconsistent without the elim restriction (it is indeed because of impredicativity). Here's a link to the lecture notes: https://courses.ps.uni-saarland.de/icl_18/dl/127/LN-13.pdf
It's a super cool proof IMO, because it's so close to the "usual strange loops".
The lecture notes also demonstrate why type universes are needed and his similar the reasons really are!

La dernière infographie qui tue sur les réseaux sociaux :

This transcends language

Cool comic by Ryan Estrada, one of my favorite comic artists, about the complexity of gender identity, identity in general and diversity.

C'est un peu cela, parfois, mais heureusement c'est de plus en plus rare 😉
https://marketoonist.com/2018/10/transformation.html

"La domination au travail est donc beaucoup plus dure qu’avant. Elle a changé complètement le monde du travail et même toute la société. Pour le dire autrement, les gens sont soumis. En Europe, les contre-pouvoirs, les syndicats, ont fondu. Ce qui fait la force incroyable du système, c’est que la majorité des travailleurs vivent dans cette situation de servitude volontaire – et donc de malheur – parce qu’ils y consentent"

Christophe Dejours

https://www.lecho.be/opinions/carte-blanche/christophe-dejours-la-domination-au-travail-est-beaucoup-plus-dure-qu-avant/10060958.html

Bio = -25% cancer d'après https://mobile.lemonde.fr/planete/article/2018/10/22/l-alimentation-bio-reduit-significativement-les-risques-de-cancer_5372971_3244.html

Seuls les commentaires apportent la nuance : bio POURRAIT être UN facteur protecteur du cancer du sein chez la femme ménopausée et cancer du sang (LNH) mais pas les autres types de cancers et facteur de risque pour d'autres (ex: prostate) !

Et encore bien d'autres nuances...

"Ferrero rossé", mon dessin du jour pour 7sur7 https://myprivacy.persgroep.net/?siteKey=atXMVFeyFP1Ki09i&callbackUrl=https://www.7sur7.be/7s7/privacy/callback.do?redirectUri=/7s7/fr/9104/Belgique/photoalbum/detail/3345382/1611960/0/Les-dessins-de-Marc-Dubuisson.dhtml

https://twitter.com/Unpied/status/1054274622835834880