I made some slides on trying to understand equality https://docs.google.com/presentation/d/1Z1i38i4_mtW11_0KmbYz1o2SwjtlaWHB1j_cZyQ0Mr4/edit
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.
https://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.
I just verified that an S-expression parser recognizes only S-expressions.
Implementation: 250 LOC
Spec: 125 LOC
Proof: 700 LOC
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...
Un truc que je ne comprends pas sur les trous noirs
@MartinShadok
J'y connais techniquement rien, donc à prendre avec des gros grains de sel. Je crois que les singularités ce sont plutôt des phénomènes qui apparaissent dans les modèles théoriques, qui indiquent qu'on est à des échelles où ces modèles ne sont pas fiables. Bref, quand des équations disent que quelque chose tend vers l'infini, en réalité il y a probablement un mécanisme inconnu qui prend les devants.
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] https://github.com/coq/coq/issues/10597
[2] A related discussion https://coq.discourse.group/t/would-coq-benefit-from-docstrings/849/3 and an idea floating around is to build something on top of OCaml's odoc.
@lthms
Great! Thanks!
@lthms
That's the third thing I broke with that patch... I should work on some tests around that part...
@lthms
Oh I see. I misunderstood the syntax of begin details, thought it was a standalone tag like the others. Sorry about that.
@lthms
new_lines is called to update the current position for errror reporting, so it might be something else I did...
Haskell and Coq programmer