Isn’t part of the bloat that the instruction sets of these platforms are also bloated? The Intel manual is quite large. Are we close to compiling towards the o

Isn’t part of the bloat that the instruction sets of these platforms are also bloated? The Intel manual is quite large. Are we close to compiling towards the optimal code for Intel chips? If we could achieve that then we’d at least be in lock step with the hardware… But syntactically and semantically we’re kind of stuck in the stone ages. We’ve had languages that can compress a ton of information into a single combinator for some time but the dominant mode of thinking in industry is procedural. I wonder if Eliot is right and the way forward at a certain scale is through correct software: designed and compiled from dependently typed languages with the aid of theorem provers.