I think this article would be better if it ignored the issue of proving termination.
Proving that a program terminates eventually is a very weak guarantee, since it could be a program that terminates after a million years. This matters mostly for proof languages, where it’s useful to write proofs about functions that you never run. If the function provably terminates, you can assume that whatever value it returns exists, without calculating it.
For a possibly long-running job like a SQL query, a static guarantee that it terminates eventually is almost certainly not what you want. You’re going to need to test its performance, and ideally have a timeout and a way of handling the timeout. If you want to get fancy, a progress bar and cancel button might be nice.
Edit:
Compilers need to run fast for the programs we actually write. A type system that possibly doesn’t terminate under unusual conditions isn’t that big a deal, as long as people don’t write code like that. Hopefully you get a decent error message.
Compare with memory use. We don’t want compilers to use excessive amounts of memory, but don’t need static guarantees about memory use.
Proving that a program terminates eventually is a very weak guarantee, since it could be a program that terminates after a million years. This matters mostly for proof languages, where it’s useful to write proofs about functions that you never run. If the function provably terminates, you can assume that whatever value it returns exists, without calculating it.
For a possibly long-running job like a SQL query, a static guarantee that it terminates eventually is almost certainly not what you want. You’re going to need to test its performance, and ideally have a timeout and a way of handling the timeout. If you want to get fancy, a progress bar and cancel button might be nice.
Edit:
Compilers need to run fast for the programs we actually write. A type system that possibly doesn’t terminate under unusual conditions isn’t that big a deal, as long as people don’t write code like that. Hopefully you get a decent error message.
Compare with memory use. We don’t want compilers to use excessive amounts of memory, but don’t need static guarantees about memory use.