> 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.