Comment by keithwinstein

This is really cool stuff, and I agree the future is likely to look more like this. I was surprised by the last two paragraphs ("Aside: verified assembly") -- my understanding was that this future is basically already here. I believe agl's colleagues at Google have already deployed some auto-mutated verified assembly versions of some crypto routines, based on the Fiat Crypto + CryptOpt work (https://arxiv.org/pdf/2211.10665), both involving Andres Erbsen who I think is currently at Google before starting a professorship soon. I dunno if this work would count as "cheap" (it looks like Fig. 10 unfolds over the course of a day) but spending a day auto-exploring many verified-correct machine code implementations of the same routine to find the fastest one (which you then ship forever) doesn't seem impractically expensive either.