"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.