[wtroughton]

A compiler is a theorem prover, sure, but compilers vary in terms of expressiveness of the propositions it is capable of proving (a Python interpreter would be a very weak theorem prover ;) )

Consider: is there an equivalent concept of Turing Completeness for compilers with respect to computational propositions?