The halting problem states that it's impossible to know if computation will terminate in the general case, but there are lots of specific cases where we can pro

The halting problem states that it's impossible to know if computation will terminate in the general case, but there are lots of specific cases where we can prove that it will terminate. The Idris language compiler (think haskell with dependent types) will actually warn/error if you've written a function that it can't prove will terminate. It's actually really cool! If you're interested in learning more, I'd check out any talks by Edwin Brady or pick up his book[0] [0]Type-Driven Development with Idris