And what of Lisp, of which most dialects have mutable state? If a Lisp compiler would convert to genuine λ-calculus it would be as large a step as it would for C.
My point was that although there are functional languages that are syntactic sugar over the lambda calculus, I don't know of any imperative languages (and in fact it would not make sense to design an imperative language) that is syntactic sugar over turing machine code.
I should have made my position clearer. I do agree that compiling any non-pure functional language via lambda calculus is a fruitless endeavor.