> Author complains about the inability of the compiler to prove some property of his code.

No, the author is complaining about the complexity of the language. Maybe you should go back and re-read the article. Start with the title.

> Untyped languages

Lisp is not untyped. "Not statically typed" is not synonymous with "untyped."

> Therefore, you are completely missing the point.

Which of us is missing the point remains to be seen.