Hilbert's program was about whether every statement could be proved ab nihilo either true or false. The question remains: given a proof, can we verify it? Arguably, any proof conceived by a human mind should be verifiable in principle. So the Incompleteness Theorem doesn't really apply, either formally or morally.

A more interesting argument could be made on the basis of Rice's Theorem: for a Turing-complete language, the only non-trivial properties provable about a program are fundamentally syntactic. (Type systems can be seen as a way of elaborating your syntax to capture finer-grained details of your semantics). Here we have a richer and nearer-to-hand collection of programs whose properties are inaccessible -- take, for instance, whether the 3n+1 algorithm halts on all inputs. Again, though, if we have a proof of some property, we still ought to be able to verify it.

Isn’t verifying a proof equivalent to determining whether a certain computer program halts?

No, but it would be equivalent to verifying that a given computer program halts on a specified N steps.

This is the same distinction between (among other things) P and NP problems. For any problem in P, given an instance of the problem I can produce a solution in polynomial time. For any problem in NP, given an instance of the problem and a candidate solution, I can determine whether the solution is valid in polynomial time.

Determining whether a certain computer program halts would be equivalent to producing a proof, not verifying an existing one.

Verifying a proof is, in principle, only a matter of making sure that each step of the proof is valid. Coming up with the right steps is a creative endeavor. Certainly, coming up with the right set of allowable steps is a creative endeavor, and proving that your system is expressive enough for interesting proofs is a creative endeavor. But once given a proof, verifying that it legally applies legal steeps is a purely mechanical endeavor.

> But once given a proof, verifying that it legally applies legal steps is a purely mechanical endeavor.

But isn't this the same as once having a program then executing it? which then has the problem of does it finish? so back to the halting problem?

No, because a proof (especially a human-constructed proof) is a finite object built out of basic pieces. The only question as to the validity of a proof is whether the basic pieces have been fit together according to the established rules of the game. We don't have to have any notion of "execution" of a proof to verify that its construction is valid.

Let me put it this way. I tell you that I can make apple juice if you give me an apple and a juicer. Do you have to give me anything to believe me?

Several researchers have indeed put together a theory of "execution" of a proof; see for instance Prof. Frank Pfenning's research program on logic-based process calculi. These theories tend to have the common theme of execution as normalization -- the chosen mode of execution actively changes and evolves the proof structure until it reaches a terminal form, usually one with a particularly simple logical structure. Cut elimination is a central theme: any logical system worth calling "computational" (one argues) will support cut elimination, allowing you to replace a proof with steps like `A -> B, B -> C |- A -> C` with a direct proof of `A -> C` that does not use the intermediate hypothesis `B`.

But we're not doing that when we're verifying a proof. We're looking at the finite, static structure of a proof term, and checking that it was put together legally.

The problem with Hilbert’s program was, loosely, that the power to construct propositions was stronger than the power to mechanically check proofs. That is, the formal language of propositional logic + number theory can construct propositions that are not decidable in a finite number of steps.

There are two responses to this discovery: tweak the formal system so you can’t accidentally run into these traps, or shrug and just be more careful about how you prove things.

Now that the world is increasingly computerized, it’s become clear that the right choice is to stop using a default form of mathematical reasoning that causes major issues for mechanized proof assistants and instead build a new foundation that is friendly to computers (but can be extended to support the power of classical formalisms)

Parent is referring to something a bit different - Hilbert’s program was about all of mathematics, even that which hadn’t been discovered yet, whereas the parent is talking about formalizing existing mathematical knowledge in some HoTT-enabled programming language or proof-checker (hence the emphasis on verifying and the problem of siloed knowledge).

Obviously true theorems with existing proofs don’t apply to Godelian incompleteness.