I attended djb's ETAPS talk and am still not true if he was deliberately provocative or genuine. Assuming the latter, I disagree with several of his points. Her

I attended djb's ETAPS talk and am still not true if he was deliberately provocative or genuine. Assuming the latter, I disagree with several of his points. Here I want to bring one to the readers' attention and it's to do with the economics of correctness proofs. One of his key arguments was that compiler optimisations are difficult to prove correct, and that's one of the reasons why optimising compilers will be replaced by a combination of simple compilers + assembly hand-written by domain experts. It is true that such proofs are (currently) expensive, but misses the point of the economics of correctness proofs: Correctness proofs are difficult, but proving compilers correct amortises that cost over all subsequent uses. In contrast, program specific correctness proofs are typically of comparable difficulty, but don't amortise in this way. Therefore it seems to be cheaper in the long run, to focus on the correctness of optimising compilers. Moreover, as compilers and optimisations are quite a restricted class of algorithms, hence it is more likely that we can reuse (parts of) correctness proofs and prover technology for compilers.