Comment by jasongross

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.