9 ms·
Godel's theorem only applies to proof systems that can encode basic arithmetic, which most type systems cannot.
by snnw 9y ago
Godel's theorem only applies to proof systems that can encode basic arithmetic, which most type systems cannot.
- vanderZwan 9y agoWould a type system that can verify whether array access is always in-bound implicitly encode arithmetic somehow? My gut feeling says yes, since I don't know how one would prove bounds without arithmetic, but I don't have the mathematical knowledge to back this up.
- lmm 9y agoIt would need a certain amount of arithmetic, but Presburger arithmetic (addition and constant multiplication, essentially) is complete and consistent and might be enough for all the array use we care about?