4 ms·
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
by somewhereoutth 7y ago
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.
- abathologist 7y agoCTT 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.
- pjc50 7y ago.. 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)