That language with your described properties already exists and is called SBCL (http://www.sbcl.org/ http://www.sbcl.org/). I'm not sure what you're arguing at

That language with your described properties already exists and is called SBCL (http://www.sbcl.org/ http://www.sbcl.org/). I'm not sure what you're arguing at this point though and don't quite get what point you're making. Compilers, optimizations, type systems, and proof systems are all very closely related and if you want correct optimizations then you must annotate your code with types that the compiler can verify and use as assumptions in an optimization pipeline. These things are not easy to engineer. Saying just JIT it doesn't make much sense.