No, 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.
Yes, 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.
> 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!
No, 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.
He 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.
Yes, 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.
> 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!
Indeed! But I am afraid general purpose programming languages almost always need that kind of power (though being Turing complete is not necessary)
1 reply →