4 ms·
>Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs! You'll never understand beca
by shikoba 5y ago
>Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs!
You'll never understand because it's false. Godel theroem proves that theorems aren't enumerable. But they're still computably enumerable.
- reuben364 5y agoA more degenerate argument: a type system that rejects all programs will prevent all bugs.
- Koshkin 5y agoI have seen programmers 1) design a type hierarchy; 2) struggle getting things compiled; 3) give up.
- ProfHewitt 5y agoTheorems of a foundational system are not computationally enumerable (in fact they are not even countable). See the following article: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021 In a foundational system, there are true propositions that cannot be proved. For example, is true but unprovable that an algorithm can enumerate the theorems of an order abstracted from strings.
- shikoba 5y ago>there are true propositions that cannot be proved In that case, they're not theorems. Theorem are things that can be proved starting from axioms. And proofs are enumerable, except if the axioms are not enumerable.