I think it would be much more fruitful to flip it around the other way. Start with small pieces which halt, and see how far you can get by combining them into

I think it would be much more fruitful to flip it around the other way. Start with small pieces which halt, and see how far you can get by combining them into larger programs. Compiler-help is available: https://docs.idris-lang.org/en/latest/tutorial/theorems.html#directives-and-compiler-flags-for-totality https://docs.idris-lang.org/en/latest/tutorial/theorems.html... A down-side of a yes/no/maybe halting checker is that it wouldn't tell you why. You'd get your "doesn't halt" result and then have to debug the algorithm.