You make a compelling argument, but, empirically, when you optimize code for performance, you end up with an unreadable mess that breaks all abstractions; but every time I've substantially optimized a proof for performance [of proof checking], I've ended up with better abstractions and more modularity.
That's super interesting. I wonder if you've tried optimizing for type-checking duration of a richly dependently typed program and gotten viscerally nicer code out of that.
Yes, but usually the thing that comes out of this process is having less rich types and separating proofs from computation. (Example: working with length-indexed lists in https://github.com/mit-plv/fiat-crypto was a lot more painful for writing cryptographic algorithms than using plain lists and proving length-preservation separately with tactics. Probably because the length is not an inherent part of the algorithm.)
loading story #50218053