He's writing yacc for crypto protocols. You write an algorithm in his Stupid language, you and others verify it Stupidly, and then compile it to your real language.
So the language's compiler does analysis of the algorithm for common crypto flaws? (like buffer-overruns and timeable iterations ...)?
Nope. It does nothing at all except to standardize the notation.