lyxia boosted

💻 C'est quoi un programme "prouvé" mathématiquement ?

Apprenez-en plus avec le nouvel article de Aabu :
Écrire des programmes prouvés corrects avec Coq (🐓)
zestedesavoir.com/articles/375

#ZesteDeSavoir #programmation #Coq

What if nothing is real and everything is an abstraction

Fun challenge by Talia Ringer on twitter:

How fast can you prove

N.succ (N.add x y) = N.add x (N.succ y)

without stdlib lemmas? As in, pretend you only just defined N and its operations.

NB: this is the binary N, not the unary nat, so it's a bit trickier than it looks.

(The starting import is "From Coq Require Import NArith.")

- I was born on a year of the Rooster
- I learned Coq on a year of the Rooster

🤔

lyxia boosted

"these models are vulnerable to a kind of “typographic attack” where adding adversarial text to images can cause them to be systematically misclassified."
📄 distill.pub/2021/multimodal-ne

lyxia boosted

When asked about fears of automation in 1969, Arthur C. Clarke famously said that we shouldn't worry about automation: "the goal of the future is full unemployment, so we can play." I have never seen his answer quoted in full.

Ancient egyptians worshipped cats, because cats inspire awwe.

Can we say that functions in cubical type theory are CuTT Pi's?

lyxia boosted

This channel has an extremely weird and fun aesthetic. A material scientist telling silent stories while making kitchen knives from things that shouldn’t be made into knives.
youtu.be/GMS6AoXKMeQ

J'ai un fichier de N octets. J'alloue un tableau de N octets. Je lis N octets. Erreur dans Windows, EOF exception. Parce que les \r\n sont convertis en \n, le tableau va contenir moins de N octets. Ok, je fais attention de bien m'arrêter à la fin du fichier. Deuxième erreur, j'ai des \0 à la fin des sorties. J'étais encore en train de dire au reste du programme que le tableau faisait N octets. Pfiou.

lyxia boosted

Haktoberfest is a nice idea with a terrible execution. Letting repos opt in would basically solve the spam problem.

I just verified that an S-expression parser recognizes only S-expressions.

Implementation: 250 LOC
Spec: 125 LOC
Proof: 700 LOC

github.com/lysxia/coq-ceres

Apparently parser combinators in total languages with dependent types is still a widely open research problem. Projects that need parsing just roll their own stuff, and rarely verify it...

github.com/gallais/agdarsec

To git rebase whenever you pull, add in ~/.gitconfig :

[pull]
rebase = true

Communication is hard. I don't want to sound like an obnoxious smartass when disagreeing with someone at work.

Show older
La Quadrature du Net - Mastodon - Media Fédéré

Mamot.fr est une serveur Mastodon francophone, géré par La Quadrature du Net.