> but solving the halting problem would also be very valuable. The halting problem is mostly a non-problem in settings that really need a proof. We have non-tu

> but solving the halting problem would also be very valuable. The halting problem is mostly a non-problem in settings that really need a proof. We have non-turing-complete languages that let us produce programs that provably halt. That they are not mainstream tends to show that we don't really need that proof very often actually.