Related but more high level, I think we should have language sets instead of single languages with simpler interop and shared infra: https://gist.github.com/xixixao/8e363dbd3663b6729cd5b6d74dbb...
Common lisp can be and has been successfully used for high-performance numerics[0] as well as low-level system code[1], all while being a high-level, garbage-collected language. (The latter property likely leading to better overall performance in large programs.)
Verification may be interesting, for high-assurance (e.g. automotive/aerospace) applications. It's for this reason that a theorem prover[2] and an ml[3] have been implemented, and they interoperate freely with the rest of common lisp.
In other words: we are already where you want to be, and we are even less stratified than you propose we would need to be.
0. https://github.com/marcoheisig/Petalisp
1. https://github.com/froggey/mezzano/