&gt; Gödel doesn&#x27;t say anything about &quot;non-trivial&quot; any more than Turing does.<p>Source: <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Halting_problem" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Halting_problem</a><p>Quote: &quot;Rice&#x27;s theorem generalizes the theorem that the halting problem is unsolvable. It states that for any <i>non-trivial</i> property, there is no general decision procedure that, for all programs, decides whether the partial function implemented by the input program has that property. (A partial function is a function which may not always produce a result, and so is used to model programs, which can either produce results or fail to halt.) For example, the property &quot;halt for the input 0&quot; is undecidable. Here, &quot;<i>non-trivial</i>&quot; means that the set of partial functions that satisfy the property is neither the empty set nor the set of all partial functions.&quot;<p>Source: <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;G%C3%B6del%27s_incompleteness_theorems" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;G%C3%B6del%27s_incompleteness_...</a><p>Quote: &quot;Gödel&#x27;s incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of <i>all but the most trivial</i> axiomatic systems capable of doing arithmetic.&quot;<p>&gt; It would be nice if we could verify Coq in Coq itself ...<p>I was planning to bring this issue up, but you&#x27;ve done it for me. The simplest explanation of these two related theorems involves the issue of self-reference. Imagine there is a library, and a very conscientious librarian wants to have a provably correct account of the library&#x27;s contents. The librarian therefore compiles an index of all the works in the library and declares victory. Then Gödel shows up and says, &quot;On which shelf shall we put the index?&quot;<p>In the same way, and for the same reason, non-trivial logical systems cannot check themselves, computer languages cannot validate their products (or themselves), and compilers cannot prove their own results correct.<p>&gt; And it seems to be worthwhile to prove things correct in a proof assistant, even without a computer-checked proof of that proof assistant&#x27;s own correctness.<p>Yes, unless someone is misled into thinking this means the checked code has been proven correct.<p>&gt; This is not waving away the problem ...<p>When someone declares that a piece of code has been proven correct, in point of fact, yes, it is.