TLDW: Godel's incompleteness theorem is at odds with the goals of Principia.

I remember my Java IDE in undergrad warned me about an infinite loop, and this was before I learned about the diagonalization proof of the non-computability of the halting problem, one of my favourite proofs ever. The fact that not all programs and inputs can be shown to halt did not stop the engineer who wrote that guardrail for the IDE.

Surely the principia and similar efforts will still yield useful results even if they cannot necessarily prove every true statement from the axioms?

Which is weird because he used the formalism of principia to actually state the theorem, or at least part of it