Show newer

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.

I just realized I have a Windows machine, that I could use to test the portability of stuff. I didn't realize earlier because I spend so much time in a Linux VM...

coqdoc is packaged as part of Coq, so projects stuck on older versions don't benefit from bugfixes and new features. That's sad. I've been wanting to split it off[1] but actually the whole thing should be redesigned from scratch[2] so it doesn't seem worth it to break things only to break them again shortly after.

[1] github.com/coq/coq/issues/1059
[2] A related discussion coq.discourse.group/t/would-co and an idea floating around is to build something on top of OCaml's odoc.

lyxia boosted
lyxia boosted

Proving Algebraic Datatypes are “Algebraic” in #Coq
soap.coffee/~lthms/posts/Algeb

It was fun to write, hope you enjoy reading it. I tried to spellcheck it, but tbh I wouldn’t be surprise to find mistakes… If you notice some, feel free to tell me!

woohoo, 4h to the deadline, arguing with coauthors about whether a proof is correct (luckily entirely nonessential either way)...

lyxia boosted

I’ve finally started to work on my next blogpost: Why algebraic datatypes are “algebraic,” explained.

Inspired by @na and her nice write-up (in French, here blog.gelez.xyz/type-produit/)

Proofs are done[§], I need to actually write the explanation now x).

[§]: gist.github.com/lthms/8f93f3c4

lyxia boosted
lyxia boosted

Goldman's new "free" typeface has a license that prevents you from using it to criticize Goldman Sachs.

Whoops

lyxia boosted

HTTP status emojis:

- 200 👍
- 201 🆕
- 301 👉
- 400 👎
- 401 🔒
- 402 💰
- 403 🚫
- 404 🤷‍♂️
- 408 ⌛️
- 410 💨
- 418 🍵
- 500 💩

(via francesc)

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

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!