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
362 karma · joined August 1, 2014
Here is how you can prove the first theorem in Dafny. https://rise4fun.com/Dafny/GxplK
https://thefeedbackloop.xyz/stroustrups-rule-and-layering-ov...
Rust is best for complex systems where tight control of resources is required.
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.
https://dl.dropboxusercontent.com/u/12405967/ANSsem.pdf
Not sure exactly when repcodes were invented. Igor Pavlov has already used them in 7zip.
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.
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...
echo $'hello\nworld'
it's really fast to push the 16*64 bit registers to the stack
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.
https://treasurytoday.com/2014/05/algorithm-appointed-to-inv...
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.
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.
See the cover of this book by Smullyan http://ecx.images-amazon.com/images/I/81y-bMMYCoL.jpg