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-co

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 https://github.com/marcoheisig/Petalisp 1. https://github.com/froggey/mezzano/ https://github.com/froggey/mezzano/ 2. https://www.cs.utexas.edu/users/moore/acl2/ https://www.cs.utexas.edu/users/moore/acl2/ 3. https://github.com/coalton-lang/coalton https://github.com/coalton-lang/coalton