just wait a second...

An article of faith is that the undecidability of the halting problem makes it impossible to restrict to terminating programs and still have a general-purpose programming language. On the other hand, another article of faith is that we'd be in big trouble if we allowed non-terminating proofs in mathematics (e.g., "Trust me, I have a proof of the Riemann Hypothesis, just wait a second..."). Why the double standard? Do we shackle ourselves by using a fragment of mathematics that disallows (we hope) non-terminating proofs? Or have we been too hasty to accept non-terminating programs? The latter stance is embraced in total functional programming. But I think the former is also not super crazy. With a more interactive notion of proof, potential non-termination would not be so dangerous.

Z: "I have a proof of the Riemann Hypothesis, can you add it to the Book?"

E: "Of course, but first can you tell me how you handle this tricky case?"

E presents tricky case to Z

Z: "Sure, no problem, this case is easily handled by, um, some math, er, ..."

Z stalls

E waits patiently, but keeps the Book firmly shut

In some sense, terminating proofs are just a time-saving mechanism for referees. It would indeed be a shame if Z wasted all of E's time with this pseudoproof of RH. On the other hand, E could be doing other things at the same time, such as drinking coffee, or running SETI@Home.