Re:Where do type systems come from? (2017)
by reuben364 on Friday October 01, 2021 @04:34PM
(#28723135)
A more degenerate argument: a type system that rejects all programs will prevent all bugs.
Re:Where do type systems come from? (2017)
by Koshkin on Friday October 01, 2021 @05:15PM
(#28723460)
I have seen programmers 1) design a type hierarchy; 2) struggle getting things compiled; 3) give up.
Re:Where do type systems come from? (2017)
by ProfHewitt on Saturday October 02, 2021 @07:49PM
(#28733240)
Theorems 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
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.
Re:Where do type systems come from? (2017)
by shikoba on Friday October 08, 2021 @04:59AM
(#28797135)
>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.
You'll never understand because it's false. Godel theroem proves that theorems aren't enumerable. But they're still computably enumerable.