250 karma · joined July 5, 2015
https://aosabook.org/en/llvm.html
Based on that, my understanding was that while intermediate representations were certainly not new, being strict about not mixing the layers was still quite rare. He specifically claims that GCC's GIMPLE is (was?) not a fully self-contained representation.
I'm not an expert in any of this. Just sharing the link.
The notation "0.999..." looks non-threatening, which tricks people into believing that they understand what it means. We could make "0.999... = 1" look scarier by writing it as [n ↦ 1 - 10^(-n)] = [n ↦ 1], where [n ↦ a_n] denotes the equivalence class of a Cauchy sequence of rational numbers. These statements mean the same thing, but with the scarier notation much fewer people would mistakenly believe that they understand what it says.
I would expect mathematics majors to learn what 0.999... means during their undergraduate university courses. But then there's still the question of why mathematicians chose to define it that way. To really understand that, you need to be able to come up with alternative definitions and to investigate the consequences of those definitions. And for most undergraduates, it might still take a few years to build that level of mathematical maturity.
For anyone who is not a math major, I certainly don't want to discourage any curiosity about this subject. Just don't be discouraged if you feel you can't fully understand what's going on. Understanding what 0.999... means and why mathematicians chose to define it that way is quite subtle.
I use a traditional password manager. If an attacker, perhaps with a hidden camera, managed to see me type my master password, then they would still need access to one of my devices before they can use it. And if I had any idea that my master password might be compromised, I would change it just in case. It's quick and easy.
With deterministically generated passwords, all of my passwords would be compromised the moment my master password is compromised. I might not even _have_ a complete list of all the passwords that I should now remember to change. And I wouldn't do it lightly, because it's far from quick and easy.
Also, if a single generated password leaks, then an attacker could use that to start brute-forcing my master password. It's nice and all that there is PBKDF2 to slow it down, but the situation is still worse than with a traditional password manager, where one leaked password doesn't reveal any information about the other passwords.
Suppose the question was instead: "What is the unique real number x for which x^3 = 8?" We can guess and verify that x = 2 is a solution. And if we're allowed to assume that this equation has a unique solution, then that's enough. But if we work a little harder, then we don't actually need that assumption: we can prove that x = 2 is the unique solution.
Similarly, in the original problem we could guess and verify that FFFFTF is a solution. And if we're allowed to assume that the solution is unique, then we're done. But again, if we work a little harder, then we don't need that assumption: we can prove that FFFFTF really is the only solution.
But when I program, then "trying to find any program that has a given type" rarely feels like the main problem I'm trying to solve. Depending on the program, I may want the program to do any of these things: run efficiently, conserve memory, have a good-looking and intuitive user interface, support multiple languages, be secure, be maintainable. If it's a web app, I want it to support multiple browsers. If it's a game, I want the challenge level to be just right. If it's a software instrument, I want it to sound good. You get the idea. So yes, there exists an isomorphism between programs and proofs, but I'm not really sure what to do with it, since the isomorphism doesn't preserve most of the properties I care about.
If that was a common feature in formatting tools more than a decade ago, then I missed it too.
Maybe this is not a lucrative opportunity for someone who also has the skills to gather a botnet that consists of millions of computers. But this attack requires minimal skills. If Gmail didn't use HTTPS, there would be an easy-to-use Gmail hacking app. If Facebook didn't use HTTPS, there would be an easy-to-use Facebook hacking app. The risk of getting caught is small. And by going to the right place, there's a reasonable chance of targeting a particular person, which many would find appealing. I think that the only reason attacks like this aren't more common is that most of the high-value attack targets are already using HTTPS.
Maybe I misunderstood, but it sounds like you're criticizing HTTPS for its success. People only rarely get hacked using man-in-the-middle attacks, because popular sites are already using HTTPS. If they didn't, I'm sure they would be MITM-hacked all the time.
UTF-8 is one to four bytes, UTF-16 is two or four bytes, and UTF-32 is always four bytes. For some code points, UTF-8 is 50% longer than UTF-16 (3 vs 2), but UTF-8 is never longer than UTF-32.
But it is not the only perspective one can take. Allen Newell, Alan J. Perlis, and Herbert A. Simon argue that computer science is the study of computers [1]. I think this is also an insightful thing to say, and it is good to try to understand why they would say that.
And even if I disagreed with them, I still wouldn't dismiss all writings of three (!) Turing-award winners based on a single wrong opinion.
It is an established convention in mathematics to write definitions in the form "X is Y if P(X)". For example: "A metric space M is complete if every Caychy sequence in M converges in M".
One may question whether this is a good convention, but it is a convention that most mathematicians tend to follow.
As many other commenters here, I mostly rely on password autocompletion. If autocompletion doesn't recognize the site, then I'm extra careful. The point is that this is rare enough so that it is actually feasible for me to be careful on those occasions.
For example, here is my "formal definition" of a primality checker:
IsPrime(Int n) = n > 1 and not(exists a, b in Int: a > 1 and b > 1 and a * b == n)
It is not directly executable, because it uses the "exists" quantifier over all integers. A clever code extractor should be able to somehow convert this to a finite computation. But would it be able to come up with the polynomial-time AKS primality test? [1] I highly doubt it.
Unless, of course, there is a special case for recognizing this particular definition. But I don't think that really counts, because I'm only using primality checking as an example. You can't have a special case for everything.
Roughly speaking, Gödel's incompleteness theorems say that all proof systems for number theory are limited in some way. For example, first-order Peano arithmetic is such a system, and one of its limitations is that it doesn't support transfinite induction. (It doesn't matter if you don't know what it is.) In other words, if you want to translate a mathematical proof to Peano arithmetic, you have to come up with a way to do it without transfinite induction. Sometimes, such in the case of Goodstein's theorem, this is impossible. To prove Goodstein's theorem, you have to choose a stronger proof system to begin with.
So, Gödel's theorems guarantee that no matter how strong you proof system is, there are always number-theoretic statements that are beyond its reach. But for reasons that are not currently completely understood, this doesn't really happen in practice. "Naturally occurring" examples of number-theoretic statements almost always turn out to be provable in surprisingly weak systems.
Instead, you run into practical problems: the theorem is provable in the system, but actually writing out the proof is utterly inconvenient. As an analogy, there are Turing-complete programming languages that don't have the concept of functions. In theory, they are capable of all kinds of computations, but in practice you don't want to use them.
And if, instead of mathematics, we concentrate on proofs of correctness, then this is even less of a practical problem. To quote Leslie Lamport, proofs of correctness "are seldom deep, but usually have considerable detail." The proofs may be long and complicated, but as long as they don't use any kind of ridiculously abstract techniques, they are just the kind of proofs where computers can have an advantage over humans.
What I should have said that harmony is less ad hoc; it has less "degrees of freedom".
With regards to melody, there are tons of tuning systems that are quite close to the usual twelve-tone equal temperament. It would be hard to give a convincing argument that one of these sounds better than all others.
Contrast this to the system of harmony where the basic principle is that ratios of small integers sound good together. This is not the only possible system of harmony, but it does seem to represent some kind of local optimum. And this makes it more amenable to the kind of purely theoretical reasoning that the article is trying to do.
First of all, let's focus on harmony (notes played at the same time) as opposed to melody (notes played one after another). What sounds good in a melody is quite culture-dependent, but there are reasons why harmony is more universal.
Second, let's focus on sounds that are produced by something long and narrow. In a guitar, violin, or piano it's a string, and in a flute it's a column of air. The physics of vibrations goes so that in such a case the sound is composed of harmonics: sine waves of frequencies f, 2f, 3f, 4f, ... If the shape is different (say, a circular membrane of a drum), then this may not apply.
Suppose we add a second sound, whose fundamental frequency is, say, 3/2 f. This means that its harmonics are 1.5f, 3f, 4.5f, 6f, 7.5f, 9f, ... Half of these (3f, 6f, ...) coincide with the harmonics of the first sound, so the sounds "reinforce" each other. More generally, if the ratio of the frequencies is p/q for some integers p and q, then there will be overlap in the harmonics. And the smaller p and q are, the more overlap there will be.
The sad thing is that the libraries use the same algorithms even if the expression doesn't contain backreferences. A while ago, Stack Overflow had a brief outage because of regular expression performance, although the expression that caused it didn't even use backreferences or other non-regular features:
http://stackstatus.net/post/147710624694/outage-postmortem-j...
In contrast, Google Code Search - when it still existed - supported regular expression searches over world's public codebases. One key ingredient making this possible was to only use proper regular expressions:
There are several ways of defining real numbers, and one of them is the axiomatic definition. Real numbers are defined by a list of axioms they must satisfy. These would include, among others:
(1) If x and y are reals, then x + y = y + x. (2) If S is a nonempty subset of reals with an upper bound, then S has a least upper bound.
There is a crucial difference between these two. In (1) the variables x and y only quantify over reals, but in (2) the variable S quantifies over subsets of reals. We say that (1) is a first-order axiom and (2) is a second-order axiom. Actually, among all of the axioms of real numbers, (2) is the only one that is second-order. Therefore, it is natural to ask: can we rid of it?
No, we cannot. Löwenheim-Skolem theorem says that if we only have first-order axioms, then it is impossible to distinguish between countable and uncountable sets - even if we have an infinite number of first-order axioms. In particular, this means that if we try to define real numbers using only first-order axioms, then the definition cannot even capture the basic fact that there is an uncountable number of reals.
From here on, there are two roads you could take. If you're like me, then you just accept that real numbers cannot be defined using first-order axioms. By my standards, any definition that only uses first-order axioms cannot be a satisfactory definition of the real numbers.
But some people don't want to accept definitions that are not based on first-order axioms. And this is not as crazy as it might sound. First-order axioms are very nice from a theoretic point of view. For example, with first-order axioms it is absolutely clear what it means to prove something based on those axioms. With second-order axioms, the situation is a lot hairier.
For untrusted certificates, the answer is clear: very severe. If https://www.facebook.com suddenly has an untrusted certificate, it is almost certainly a case of MITM. The typical end user is not in a position to make an informed decision about trusting it anyway "because it looks right", so the page should just be blocked. In current browsers, bypassing these warnings is very cumbersome. And frankly, making the warnings less conspicuous would be irresponsible.
Now, you may argue that plaintext is even worse than an untrusted certificate. But whether we like it or not, in today's internet a browser cannot just block all plaintext connections. Making plaintext warnings as conspicuous as untrusted certificate warnings is unrealistic.
That said, there are other steps browsers could take to keep pushing https. Browsers could warn when transmitting passwords unencrypted. And, I don't know if it goes too far, but perhaps browsers could even deprecate persistent cookies for unencrypted connections.
Wikipedia [1] says it was common in the 1980s, but gives two only two modern examples: Opera and Movable Type. And even that seems to be outdated. Neither of them uses decimal version numbers any more. Can you think of any others?
You might also be objecting to the fact that he makes a distinction between time and instruction count, and is using big-O notation for both. I don't think there's anything nonstandard about making this distinction when it needs to be made. Take, for example, Karmarkar's algorithm:
For comparison, suppose that someone claims that for all x, sin(x) ≤ 1/2. That would just be wrong. If someone claims that sin(x) ≤ 2, then that is true, but not as informative as saying that sin(x) ≤ 1. There's something special about 1 here. If you want to highlight that, you can say that 1 is the least upper bound for sin(x). This is a bit of a mouthful, but we cannot achieve the same meaning by just replacing "≤" by "≥" or "=" or "<". Any of these replacements would just make the statement incorrect.
Big-O is something like the asymptotic version of ≤. For example, how many comparisons does heapsort need to sort an array of length n? If someone says O(n), that's just wrong. If someone says O(n^2), then that's correct, but not as informative as saying O(n log n). O(n log n) is special here, since it is the smallest complexity class that contains the number of comparisons. Again, it is a bit of a mouthful, but we cannot say the same thing by just replacing big-O by Omega, Theta, or little-o (the asymptotic versions of ≥, =, and <, respectively). For example, Theta(n log n) and Omega(n log n) are incorrect, since heapsort only requires a linear number of comparisons if the array already happens to be sorted.
The author argues that random memory access time is O(sqrt(n)), meaning that for large n, it might take up to constant * sqrt(n) time, but might also be faster if the memory to be accessed happens to be very close. Using Omega(sqrt(n)) instead would mean that random memory access can take an arbitrarily long time, but at least constant * sqrt(n). This is not what the author is trying to say.
First, let's look at computability. The intuitive idea that some functions can be computed by an algorith is very old (think Euclid's algorithm). The idea was formalized in the 20th century by the notion of a computable function. Several different definitions were given, but surprisingly, they turned out to be equivalent. Today, most programming languages are Turing complete. As far as pure computation is concerned, it is possible to translate between different programming languages.
The idea that a mathematical statement can be conclusively proven is also very old. Again, different formal definitions emerged: provable in PA, provable in ZFC, provable in ZFC + some large cardinal axiom, etc. These are not equivalent. And this, in a sense, is one way of framing Gödel's first incompleteness theorem. There is no absolute notion of provability: no equivalent of Turing completeness; no precisely definable concept that would deserve the name "provable".
In particular, this means that it is not always possible to translate proofs from one system A to system B. At least unless you are willing to add new axioms to system B.
And using these names, I would say that preduce seems much more useful to me than reduce.
Suppose that you have a bunch of things implemented using map or filter. When someone writes parallelized versions of map and filter, all of the existing code gets the benefits.
Now suppose you have a bunch of basic functions implemented using reduce (sum, product, min, max, reverse, ...). Can these be parallelized? Yes - by throwing away the 'reduce' implementation, and starting from scratch.
The problem with reduce, compared to its more useful cousins map and filter, is that it is too powerful. Map and filter are more limited than reduce, but if you can express your computation in terms of maps and filters, you get something valuable in return. If you can express is in terms of reduce, you save a few keystrokes, and that's about it.
For anyone interested in this kind of stuff, I recommend Guy Steele's talk "Organizing Functional Code for Parallel Execution; or, foldl and foldr Considered Slightly Harmful": https://vimeo.com/6624203
Let ε be something very small, and define the difference operator d so that (df)(x) = f(x + ε) - f(x). Usually we don't want to handle the functions dx and dy by themselves, because they are so small, and their exact values depend on ε. But when we divide dy by dx we get something that is no longer ε-sized, and doesn't (in a limit sense) depend on the value of ε.
And why think way? When I learned the chain rule dy/dx = dy/du * du/dx I was told that even though the du's appear to cancel out, this is just abuse of notation and basically a meaningless coincidence. I understand that the teachers just wanted students to be careful; they don't want people "simplifying" dx/dy to x/y. However, I was never really satisfied with this explanation. I finally realized that by thinking about it using the difference operator above, it is not a meaningless coincidence: the du's actually do, in a sense, cancel out.
Article: "In functional programming, the use of lambdas allows us to propagate not merely a serialized version of our intentions, but our actual intentions!"
Counterpoint: The use of structured objects instead of black box lambdas allows us to do more than just evaluate them. For example, Redux gets a lot of power by separating JSON-like action objects from the reducer that carries out the action.
But let's take instead the article's example of case-insensitive string matching. One tricky case is that normalization can change the length of the string: we might want the german "ß" to match "SS". Sure, the lambda approach can handle that. But now suppose that we want a new function that gives the location of the first match. It should support the same case-sensitivity options (because why not?). But now there is no way to get the pre-normalization location, because we encoded our normalization as a black box function. Case-by-case code would have handled this easily.