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

[alexkcd]

I'm not sure, but I think it's different. Specifically, I think you would do macro evaluation first, then fully evaluate the resulting program on run-time independent values, and only then evaluate the resulting program on run-time dependent values.

Edit: Also, run-time independent evaluation would need to handle branching differently. For example, in this expression: (if a b c). If `a` is not known at "compile time" then this expression remains in the AST, and run-time independent value propagation continues into `b` and `c`. If `a` is known at "compile time" then only `b` or `c` remain in the AST depending on whether `a` is true or false.