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
HN user
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.
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.
Gabriel Synnaeve was already working on this long before joining FB.
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.
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.
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?There are a few (free) teaching ladders out there. The basic idea is that you have your games reviewed by players a few stones stronger than you, e.g. you are ranked around 10k and the reviewer 4k. Reviewers are strong enough to spot the biggest weaknesses in your play, so that you can improve quickly.
When I used the ladder, 15 years ago, their problem was that they had too many reviewers and too few students, so it was nice as a student :) You should give it a try.
There is already one company that took an algorithm as a voting member of its board.
https://treasurytoday.com/2014/05/algorithm-appointed-to-inv...
AlphaGo isn’t a pure neural net at all — it’s a hybrid, melding deep reinforcement learning with one of the foundational techniques of classical AI — tree-search
Most board game computer players use some sort of tree search followed by evaluation at the leaves of the tree. What we discovered in the 70s is that you don't need to have human-level evaluation to win at chess; it is enough to count material and piece activity, plus some heuristics (pawn structure, king safety...); computers more than compensate this weakness with their superhuman tree exploration.
This approach never worked so well for Go because evaluation was a mystery: which group is weak or strong? how much territory will their power yield? These are questions that professionals answer intuitively according to their experience. With so many parts of the board that depend on each other, we don't know how to solve the equation.
It looks like AlphaGo is the first one to get this evaluation right. At the end of the game, his groups are still alive and they control more territory. So Go evaluation is yet another task that used to be reserved to human experts and that computers now master. The fact that this is mixed with classical tree search does not make it less impressive.
This bot has a very flexible style. It is at ease both in calm point-grabbing positions (first game) and large-scale dogfights (see the second one), where humans used to crush computers. Lee Sedol is so strong at fighting, this is gonna be a great match between touch opponents.
How about TypeScript/TSX? React's components and "views" are easy to type (and you get completion in your IDE) but I still have to find a convenient way to type an Immutable map where each key/value pair has a different type (the equivalent of a TypeScript object). Any idea?
Section "An Example" in the middle of the page is an original description of the pipeline, from the point of view of an instruction.
Its take on probability as a way of modelling our brain is refreshing, for instance, the beginning of chapter 1:
Suppose some dark night a policeman walks down a street, apparently deserted; but suddenly he hears a burglar alarm, looks across the street, and sees a jewelry store with a broken window. Then a gentleman wearing a mask comes crawling out through the broken window, carrying a bag which turns out to be full of expensive jewelry. The policeman doesn't hesitate at all in deciding that this gentleman is dishonest. But by what reasoning process does he arrive at this conclusion? Let us first take a leisurely look at the general nature of such problems.
A moment's thought makes it clear that our policeman's conclusion was not a logical deduction from the evidence; for there may have been a perfectly innocent explanation for everything. It might be, for example, that this gentleman was the owner of the jewelry store and he was coming home from a masquerade party, and didn't have the key with him. But just as he walked by his store a passing truck threw a stone through the window; and he was only protecting his own property. Now while the policeman's reasoning process was not logical deduction, we will grant that it had a certain degree of validity. The evidence did not make the gentleman's dishonesty certain, but it did make it extremely plausible. This is an example of a kind of reasoning in which we haveall become more or less proficient, necessarily, long before studying mathematical theories. We are hardly able to get through one waking hour without facing some situation (e.g. will it rain or won't it?) where we do not have enough information to permit deductive reasoning; but still we must decide immediately what to do.
Note the weakness of the Java solution. Since its interfaces offer no support for virtual contructors (hence the design pattern), you have to instanciate a factory before you can get an empty value.
Also very challenging for chess players is retrograde analysis, where you have to find the only possible legal moves to reach the given position.
See the cover of this book by Smullyan http://ecx.images-amazon.com/images/I/81y-bMMYCoL.jpg
Looks like this React Native showcase is built with Angular!
People may have a sense of superiority, especially smart ones. Chess world champion (and genius) Bobby Fischer once said: "My opponents make good moves too. Sometimes I don't take these things into consideration".
The ability to rename a function or class attribute, accross modules, has been a great help maintaining programs larger than a few thousands lines.
Looks like a very good and fast PRNG. How could it possibly achieve higher statistical quality than a secure PRNG? I guess that depends on how you define quality.