Copied from lobste.rs since I think it'd be interesting to the audience here as well --- This “dialogue with the compiler” bit that djb lands on is in some se

Copied from lobste.rs since I think it'd be interesting to the audience here as well --- 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.