6 ms·
Godel's theorem only applies to proof systems that can encode basic arithmetic, which most type systems cannot.
by snnw 8y ago
Godel's theorem only applies to proof systems that can encode basic arithmetic, which most type systems cannot.
- vanderZwan 8y 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 8y 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?