Dear Mr. Fiedler,

please be more descriptive on what kind of recursive problems you mean. Generally speaking, primitive recursive programs without side effects (ie not touching the stack before the recursion step) are decidable.

Comptime allows arbitrary function execution, which will always terminate at compilation time due to tracking what parts were visited. The compiler therefore tracks a counter similar to the number of fixpoint iteration steps and will fail, if the amount of backwards edges becomes too big.

So one can ensure that compilation will halt after a limited number of steps. What one can not ensure is what the outcome is.

Your explanation of dependent types is missing, if and how limiting the number of steps has an influence of the type checking.

Personally I see limiting the number of possible compilation steps as sufficient for "weak decidability", since the compiler may only interpret finitely many steps akind to the Turing Machine running finitely many steps.

Could you elaborate on the underlying theory about that and add it to your blog?

Your blog post also does not differentiate between language model and implementation, which further blurs things.

Regards, Jan