Ok, we all know the new emperor will be named Trump.
But who will be Vador ?

The question is why don't they use proof of program methods over existing C ode, using external analysis tools, instead of introducing a new language ?
If C code lacks some information in order to help external analysis tools, then just add it through C comments with well defined syntax.

The state of the art for code generation is not Lisp but Pliant.
Basically the main difficulty with code generation is not to make it powerful, but have it generate meaningful error messages rather than crazy code when some bad source is submitted. Through the definition of 'Expression' and 'Instruction' notions, Pliant defined a clean way to encode a program at various stages, and the rules for the code generator. S-expresions plus syntaxical substitution with a Turing machine equivalent substitution engine as opposed to just macros will bring you the power, but only the power.
For extra details, just read the articles on http://www.fullpliant.org/