"For exatra fun: templates are turing complete _at_compile_time_, which means there's no way to prove a C++ compilation using templates will ever finish."
I mostly think you're making a good, substantial case in this article, but the hyperbole blunts the argument.
How much theorem proving have you _ever_ done with code, irrespective of language?