This “dialogue with the compiler” bit that djb lands on is in some sense obviously the right way to go forward. I’ve found this to be the case not in optimization—though I’m not in the least bit surprised to see it there—but instead in the world of dependent types. The language that the program writer writes in is often just a skeleton of the genuine information of the program. For instance, in a dependently typed program it’s often very difficult for an author to immediately write all of the complex intermediate types required to drive proofs forward, but it’s much easier to achieve this in collaboration with the compiler (really the typechecker, and e.g. via a tactics language and interactive proof general-like interface). The ultimate result, the “elaborated” program, contains much, much more information than the skeletal program the programmer originally wrote. It has been annotated by the collaboration of the compiler and the program writer to extract more of the programmer’s intention.
The same kind of thing could clearly arise from a “collaboration” over optimization. It’s even quite possible that these are the same dialogue as dependent types certainly provide much more information to the compiler about the exact properties the code ought to substantiate—in a nice, machine readable format even.
And of course Knuth put his money where his mouth is on this — TeX’s compiler has always been interested in having a dialogue with you when it encounters errors, which has never been nothing more than a nuisance to me, but that’s not because it’s fundamentally a bad idea.
Halide is an interesting here. I have only watched the video, but I find the idea neat having two sections: one for describing the algorithm and one for optimisations. http://halide-lang.org/
Very interesting! I often feel that Bernstein is the only programmer for whom we have good evidence of competence; everyone else whose code I’ve seen is clearly incompetent, a fortiori including myself.
Knuth’s quote of Hoare’s “A language should be designed so that an optimizing compiler can describe its optimizations in the source language” implies that the source language needs to be able to specify things down to the assembly level — which registers to use where, for example, not only which variables are profitable to hoist out of the loop and how much it’s profitable to unroll a particular loop. This is harmonious with Stepanov’s insistence that we shouldn’t insist that it be impossible to use unsafe constructs in our programming language, just that it should be possible to factor the unsafe constructs into libraries; and perhaps with the Coq-as-macro-assembler paper.
Also, presumably, you would like to be able to separate out the portable-algorithm aspect of your code into a separate source file from the optimizations-for-ARM aspect.
Tel’s comment about programming with dependent types is really interesting to me in this context, but I don’t have enough experience with theorem provers to really visualize what tel is talking about. Can anyone suggest good examples?
Very interesting! To elaborate on your link, it’s a 2012 OOPSLA paper by St-Amour, Tobin-Hochstadt, and Felleisen about making compilers (or rather “optimization coaches” reading compiler logs) interactively suggest optimization opportunities in your IDE; for example, “This expression consists of all fixnum arguments but is not guaranteed to produce a fixnum. Therefore it cannot be safely optimized. Constraining the arguments to be of Byte or Index types may help.”
Yeah, that makes a lot of sense! I’ve been thinking about optimizers working that way for a while. I think that the proof ideally would be stored off to the side, maybe in another file, since it’s irrelevant detail when you’re trying to read the code to figure out what it is specified to do, or prove that what it specifies is correct in terms of some larger-scale specification; and I think that sometimes you might want to just write the optimized version, and then write a proof that the optimized version has the same behavior as the unoptimized version — but that’s based on my experience that often just writing the optimized version is relatively easy, and of course I don’t have experience with any compilers that ask me to prove that x < 256 or that f is pure.
Watching the video: I’m not totally sure I understand Isabelle’s syntax (possibly listening to Skrillex is scrambling my brain), but I think they’re proving a lemma called “lem” which shows that for any positive real ε, there exists a positive (and I suppose real) δ such that for all x and y (which I suppose are also real? although that seems to be stated as a postulate of the proof, not of the lemma), if both x and y are at least equal to 1 and their absolute difference is less than δ, then the absolute difference of their reciprocals is less than ε? I didn’t totally understand the actual proof, although the theorem itself is clearly correct, because ∀x, y ≥ 1: |x-y| ≥ |1/x - 1/y|, so δ=ε is sufficient, no? It’s not obvious to me how to prove that ∀x, y ≥ 1: |x-y| ≥ |1/x - 1/y| from basic arithmetic axioms, though, or what the relevance of the ultimately have "|x - y| / |x * y| ≤ e" clause is to that proposition, though. Maybe it should be!
The “Counterexample (possibly spurious)” at 4:45, prompting a change from < to ≤ and addition of a reference to assumption #1 by the user, was pretty awesome. I love when OCaml does that with my pattern-matching. I’m not quite sure what e = ~1/1 means, but I don’t intend to demand an Isabelle syntax tutorial from you; I really appreciate you referring me to the video!
It’s an animation. View it as a slideshow. In evince, that’s F5. There is one section in the middle where he slowly fades out some text in the middle over several slides that tricked me into thinking I’d come to the end of the presentation.
The 4x3 link would be better in landscape (although it appears that due to some extra animations, it actually has twice as many pages). Perhaps you might like .ogg, too?
tl;dr: Cloudflare employed ChaCha20 in 2015 for TLS; used assembly code version, optimised for our servers' Intel CPUs (boldface by DJB) etc. He mentions that there is no non-NP-complete machine language to express all possible constraints of an algorithm (followed by some math), and at scale, hot spots will always be optimised in assembler for specific arch, and noone should really care about cold spots nowadays. Also, he pokes some fun at Wikipedia articles. :-) Fun talk.
This “dialogue with the compiler” bit that djb lands on is in some sense obviously the right way to go forward. I’ve found this to be the case not in optimization—though I’m not in the least bit surprised to see it there—but instead in the world of dependent types. The language that the program writer writes in is often just a skeleton of the genuine information of the program. For instance, in a dependently typed program it’s often very difficult for an author to immediately write all of the complex intermediate types required to drive proofs forward, but it’s much easier to achieve this in collaboration with the compiler (really the typechecker, and e.g. via a tactics language and interactive proof general-like interface). The ultimate result, the “elaborated” program, contains much, much more information than the skeletal program the programmer originally wrote. It has been annotated by the collaboration of the compiler and the program writer to extract more of the programmer’s intention.
The same kind of thing could clearly arise from a “collaboration” over optimization. It’s even quite possible that these are the same dialogue as dependent types certainly provide much more information to the compiler about the exact properties the code ought to substantiate—in a nice, machine readable format even.
And of course Knuth put his money where his mouth is on this — TeX’s compiler has always been interested in having a dialogue with you when it encounters errors, which has never been nothing more than a nuisance to me, but that’s not because it’s fundamentally a bad idea.
I wanted to add this link I should have put here in the first place: http://cs.ru.nl/~freek/courses/tt-2010/tvftl/epigram-notes.pdf
Halide is an interesting here. I have only watched the video, but I find the idea neat having two sections: one for describing the algorithm and one for optimisations. http://halide-lang.org/
Very interesting! I often feel that Bernstein is the only programmer for whom we have good evidence of competence; everyone else whose code I’ve seen is clearly incompetent, a fortiori including myself.
Knuth’s quote of Hoare’s “A language should be designed so that an optimizing compiler can describe its optimizations in the source language” implies that the source language needs to be able to specify things down to the assembly level — which registers to use where, for example, not only which variables are profitable to hoist out of the loop and how much it’s profitable to unroll a particular loop. This is harmonious with Stepanov’s insistence that we shouldn’t insist that it be impossible to use unsafe constructs in our programming language, just that it should be possible to factor the unsafe constructs into libraries; and perhaps with the Coq-as-macro-assembler paper.
Also, presumably, you would like to be able to separate out the portable-algorithm aspect of your code into a separate source file from the optimizations-for-ARM aspect.
Tel’s comment about programming with dependent types is really interesting to me in this context, but I don’t have enough experience with theorem provers to really visualize what tel is talking about. Can anyone suggest good examples?
ETA: HN discussions today and last month.
[Comment removed by author]
Something similar is Racket’s optimization coach
Very interesting! To elaborate on your link, it’s a 2012 OOPSLA paper by St-Amour, Tobin-Hochstadt, and Felleisen about making compilers (or rather “optimization coaches” reading compiler logs) interactively suggest optimization opportunities in your IDE; for example, “This expression consists of all fixnum arguments but is not guaranteed to produce a fixnum. Therefore it cannot be safely optimized. Constraining the arguments to be of Byte or Index types may help.”
Yeah, that makes a lot of sense! I’ve been thinking about optimizers working that way for a while. I think that the proof ideally would be stored off to the side, maybe in another file, since it’s irrelevant detail when you’re trying to read the code to figure out what it is specified to do, or prove that what it specifies is correct in terms of some larger-scale specification; and I think that sometimes you might want to just write the optimized version, and then write a proof that the optimized version has the same behavior as the unoptimized version — but that’s based on my experience that often just writing the optimized version is relatively easy, and of course I don’t have experience with any compilers that ask me to prove that
x < 256or thatfis pure.Watching the video: I’m not totally sure I understand Isabelle’s syntax (possibly listening to Skrillex is scrambling my brain), but I think they’re proving a lemma called “lem” which shows that for any positive real ε, there exists a positive (and I suppose real) δ such that for all x and y (which I suppose are also real? although that seems to be stated as a postulate of the proof, not of the lemma), if both x and y are at least equal to 1 and their absolute difference is less than δ, then the absolute difference of their reciprocals is less than ε? I didn’t totally understand the actual proof, although the theorem itself is clearly correct, because ∀x, y ≥ 1: |x-y| ≥ |1/x - 1/y|, so δ=ε is sufficient, no? It’s not obvious to me how to prove that ∀x, y ≥ 1: |x-y| ≥ |1/x - 1/y| from basic arithmetic axioms, though, or what the relevance of the
ultimately have "|x - y| / |x * y| ≤ e"clause is to that proposition, though. Maybe it should be!The “Counterexample (possibly spurious)” at 4:45, prompting a change from
<to≤and addition of a reference to assumption #1 by the user, was pretty awesome. I love when OCaml does that with my pattern-matching. I’m not quite sure whate = ~1/1means, but I don’t intend to demand an Isabelle syntax tutorial from you; I really appreciate you referring me to the video![Comment removed by author]
[Comment removed by author]
This is a very difficult to read PDF. The tall pages, the repeating content, it’s a dangerous game between myself and my mouse.
Are there any other summaries?
It’s an animation. View it as a slideshow. In evince, that’s F5. There is one section in the middle where he slowly fades out some text in the middle over several slides that tricked me into thinking I’d come to the end of the presentation.
+1. people post wrong links!
https://lobste.rs/s/f6qljt/the_death_of_optimizing_compilers
The 4x3 link would be better in landscape (although it appears that due to some extra animations, it actually has twice as many pages). Perhaps you might like .ogg, too?
tl;dr: Cloudflare employed ChaCha20 in 2015 for TLS; used assembly code version, optimised for our servers' Intel CPUs (boldface by DJB) etc. He mentions that there is no non-NP-complete machine language to express all possible constraints of an algorithm (followed by some math), and at scale, hot spots will always be optimised in assembler for specific arch, and noone should really care about cold spots nowadays. Also, he pokes some fun at Wikipedia articles. :-) Fun talk.