joseraul

All this may become much easier when we manage to merge proof assistants with automatic provers.

Here is how you can prove the first theorem in Dafny. https://rise4fun.com/Dafny/GxplK

One author of Xoroshiro has written a detailed (and harsh) analysis of PCG.

http://pcg.di.unimi.it/pcg.php

Rumors say he writes code in zcat to go faster.

They may not do user studies like this, but for sure they adapt to user feedback.

https://thefeedbackloop.xyz/stroustrups-rule-and-layering-ov...

Peter Norvig explains why.

http://norvig.com/chomsky.html

Gabriel Synnaeve was already working on this long before joining FB.

http://emotion.inrialpes.fr/people/synnaeve/

Don't forget the "up to". Your app may be in another section of the statistics.

OCaml is GCed and can infer more type annotations than Rust, so its code feels closer to Python.

Rust is best for complex systems where tight control of resources is required.

Such specialized filters can improve compression a lot. For instance, the e8e9 transform converts relative jumps to absolute jumps in x86 EXEs, increasing compression because lots of jumps actually point to the same address.

http://mattmahoney.net/dc/dce.html#Section_571

CPUs have gotten so complex that mastering their language (and behavior) is a skill on its own. Most people can get on with compiled/interpreted languages.

> what's 8MB when your server's got 64GB

Note that 8Mb is the size of the L3 cache on some modern Intel chips. You want fast lookups in the window area, where you constantly do random-access reads.

Indeed ANS is difficult: it is the biggest innovation in compression in the last 20 years. Its author has some nice but dense slides about it.

https://dl.dropboxusercontent.com/u/12405967/ANSsem.pdf

Not sure exactly when repcodes were invented. Igor Pavlov has already used them in 7zip.

The theoretical discussion is interesting, especially the circular library that gives some intuition of the square root law.

But in practice, you usually know the order of magnitude of your data, so access is rather O(1), for some constant that depends on the size of the data. Jeff Dean's "Numbers Everyone Should Know" quantifies this constant.

http://highscalability.com/numbers-everyone-should-know

In his excellent book [1], Andy Hunt explains what expertise is with a multi-level model [2], where a novice needs rules that describe what to do (to get started) while an expert chooses patterns according to his goal.

So, "best practices" are patterns that work in most situations, and an expert can adapt to several (and new) situations.

[1] https://pragprog.com/book/ahptl/pragmatic-thinking-and-learn...

[2] https://en.wikipedia.org/wiki/Dreyfus_model_of_skill_acquisi...

Bash equivalent is just:

  echo $'hello\nworld'

This uses ANSI C quoting https://www.gnu.org/software/bash/manual/html_node/ANSI_002d... .

TL;DR To please the gaming market, CPUs develop large SIMD operations. ChaCha uses SIMD so it gets faster. AES needs array lookups (for its S-Box) and gets stuck.

  it's really fast to push the 16*64 bit registers to the stack

Since the CPU has 180 registers (with only 16 names), why don't we need to push all 180 to store context?