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.