CTT addresses this line of thinking: http://www.scholarpedia.org/article/Computational_type_theory#A_foundation_for_computer_science http://www.scholarpedia.org

CTT addresses this line of thinking: http://www.scholarpedia.org/article/Computational_type_theory#A_foundation_for_computer_science 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.