@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 I consider a proof incomplete if it's not automated ;)

Here is my feedback from the artefact evaluation: before sending your artefact for review, consider that it might get reviewed by a human being and prepare your artefact for this eventuality. 🤔

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.

Bon. On m’a conseillé d’utiliser Eclipse. Je le lance. Je fais infuser un thé. Ça y est, il est lancé. Il ne reconnait pas mon fichier. Ah non, c’est juste que l’« aide » cache toute l’interface—y compris le fichier courant. Bon, je quitte l’« aide ». Tout plein d’erreurs. Ah. Le projet compilait très bien sans Eclipse, en fait. On me conseille d’installer un plug-in. J’essaye. Eclipse crash. Ah.
Bref, je ne suis pas convaincu.

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: courses.ps.uni-saarland.de/icl
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!

“It follows by straightforward transfinite induction” → Is this an instance of proof by intimidation? 🤔​
ocaml.org/learn/tutorials/humo

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

re: Question Coq Show more

Question Coq Show more

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

"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

lecho.be/opinions/carte-blanch

Bio = -25% cancer d'après mobile.lemonde.fr/planete/arti

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

C’est assez étonnant comment en 2018 on retrouve tout pleins de papiers scientifiques qui écrivent quelque chose de la forme « On sait analyser un language goto, donc on sait analyser n’importe quoi. ». Je ne dis pas que c’est fondamentalement faux, mais ça me semble une thèse assez étonnante.

Show more
Aleph

aleph.land is one server in the network