Comment by stewbrew

"I think that there exists a lisp with a set of axioms that split program execution into "compile-time" execution"

Common lisp macros? Pre-hygienic macros in scheme? Did I get you wrong?

The question is what is missing to implement _static_ type checking as macros and to allow the compiler to leverage the generated information.