|
| ▲ | gf000 5 days ago | parent | next [-] |
| 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. |
| |
| ▲ | kragen 4 days ago | parent [-] | | 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. |
|
|
| ▲ | naasking 5 days ago | parent | prev [-] |
| > 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 5 days ago | parent [-] | | Indeed! But I am afraid general purpose programming languages almost always need that kind of power (though being Turing complete is not necessary) | | |
| ▲ | naasking 11 hours ago | parent [-] | | They 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. |
|
|
