Ok, thanks, that makes sense. So I can sleep well at night knowing that at least my (purely assumed) understanding of Russel's dream is alive and well: we have

Ok, thanks, that makes sense. So I can sleep well at night knowing that at least my (purely assumed) understanding of Russel's dream is alive and well: we have found a formal system with axioms and inference rules (ZFC) within which all mainstream mathematics can (hopefully and in principle) be formally proven. Gödel however tells us 1) that there are mathematical "truths" (statements that always hold) which cannot be proven within ZFC, and 2) that ZFC could be inconsistent. The practical consequences of that are however limited. :) Is that a reasonable summary? :P