A problem with that is that compiler technology hasn't really progressed to do big whole-program or data-layout optimizations from high level specs. If we were

A problem with that is that compiler technology hasn't really progressed to do big whole-program or data-layout optimizations from high level specs. If we were closer to the model where a program would read its fixed inputs (for the run) and it would be specialized in place for the input using partial evaluation, with profile feedback for data accesses to help transforming the internal data representations to optimize storage requirement and cache access patterns, we would be much more motivated to specify many things abstractly enough to give machine representations of the code and data more freedoms.