&gt; Gödel didn&#x27;t prove the futility of a foundations for mathematics.<p>Your words, not mine, but Gödel did prove that a non-trivial logical system cannot be both complete and consistent. As Gödel phrased it, &quot;Any consistent axiomatic system of mathematics will contain theorems which cannot be proven. If all the theorems of an axiomatic system can be proven then the system is inconsistent, and thus has theorems which can be proven both true and false.&quot;<p>Gödel&#x27;s result don&#x27;t address futility, but completeness. That&#x27;s why his theorems have the name they do.<p>&gt; The formal system you (should) use to prove a program correct (with respect to its specification) isn&#x27;t the program itself.<p>This refers to the classic case of using a larger system to prove the consistency of a smaller one, but it suffers from the problem that the larger system inherits all the problems it resolves in the smaller one.<p>&gt; If you want to lecture someone ...<p>This is either beneath you, or it should be.