3 ms·

Aside from being able to prove that the solution halts, you mean? You get a lot of side benefits as well with a halting program, such as provable limits in time

Aside from being able to prove that the solution halts, you mean? You get a lot of side benefits as well with a halting program, such as provable limits in time and space for the totality of the program instead of just the functional core bits.

ncmncm 4y ago
Maybe you are unable to prove properties of programs you have coded in Turing-complete languages. Many of us do, though. Routinely. Quick, does this program terminate: int main() {} ? Can't prove it?
- tadfisher 4y ago
  That's not a very useful program.
  - ncmncm 4y ago
    It is the first stage of every useful program. Add to it, and show that it still terminates, uses finite memory, introduces no data races or undefined behavior, and maybe computes a step toward something useful. Repeat until done.