Comment by naasking
11 days 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!
Indeed! But I am afraid general purpose programming languages almost always need that kind of power (though being Turing complete is not necessary)
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.