Of course, that doesn't mean you can't prove anything. It just means you can't prove things generally and automatically. For example, you can't solve the halting problem in general, but you can most definitely prove that a specific program terminates, or that large classes of programs all terminate. The proof of Rice's theorem boils down to the impossibility of the halting problem.
The parent comment asks why someone would agree to a "Turing complete contract". But it's not necessary for an Ethereum contract to be "Turing complete" any more than Quicksort is "Turing complete". If the contract's code does something simple, we can verify and prove that it behaves as expected. It wouldn't be impossible to create a "safe" DAO-like contract.
But wouldn't Ethereum be a lot safer to use if its contract system would only have so many degrees of freedom, that all side effects and properties of contracts were computable for all contracts in a practical amount of time?
With the current system I imagine one could even utilize homomorphic encryption to implement another Ethereum inside Ethereum that is cryptographically protected not only against modification but also against inspection :)
I'd love to see an example of such a restricted contract language. My speculation is that we'll see a few different languages pop up with different approaches to safety, along with coding methodologies and tools for static analysis.
Maybe we'll also discover a handful of primitive contract building blocks, to be implemented with care and stringency, with methods for combining them.
The parent comment asks why someone would agree to a "Turing complete contract". But it's not necessary for an Ethereum contract to be "Turing complete" any more than Quicksort is "Turing complete". If the contract's code does something simple, we can verify and prove that it behaves as expected. It wouldn't be impossible to create a "safe" DAO-like contract.