4 ms·
I mean, since Gödel we pretty much have known that there could never be a system "without holes".
by gf000 1y ago
I mean, since Gödel we pretty much have known that there could never be a system "without holes".
- kragen 1y agoNo, that is not correct. Gödel showed that some theorems are unprovable in a consistent formal axiomatic system; he did not show that no consistent formal axiomatic systems exist.
- gf000 1y agoHe did show that every formal axiomatic system will have statements that can't be proven "from within". For these, you are left with doing a runtime check.
- kragen 1y agoYes, that's true, but then possibly we are talking at cross-purposes; when I said "numerous holes discovered in various implementations of the basic JVM type checking", I didn't mean things that needed to be checked at runtime; I meant bugs that permitted violations of the JVM's security guarantees. However difficult it may be to avoid such things at a social level, certainly there is no mathematical reason that they must happen.
- naasking 1y ago> Gödel showed that some theorems are unprovable in a consistent formal axiomatic system... ...of sufficient power, eg. that can model arithmetic with both addition and multiplication. I think the caveats are important because systems that can't fully model arithmetic are often still quite useful!
- gf000 1y agoIndeed! But I am afraid general purpose programming languages almost always need that kind of power (though being Turing complete is not necessary)
- naasking 1y agoThey need it operationally for calculations and such, but those calculations don't necessarily need to be statically validated beyond simple things like type and unit checking.