That is the point - perhaps you can't, in the same way there are true statements in Peano arithmetic that cannot be proved (if my understanding is correct). The concern is that these statements may still be useful and elegant, and ruling them out may weaken a language significantly.

CTT addresses this line of thinking: http://www.scholarpedia.org/article/Computational_type_theor...

btw, I think you're missing an important qualification, which is that a given formalism can always be enriched with new axioms to increase the scope of what it's able to prove. This is relevant for type theoretic approaches, which generally have a mechanism for adding new axioms.

.. at the cost of shipping products which have an higher chance of certain kinds of failures?

Types are not just an engineering technology, they are a QA tool.

(also, at no stage have you provided an example for such "more elegant" statements)