Comment on Idris, a language that will change the way you think about programming (2015)parentComments−kazagistar10yFrom what I know, Idris does not have this constraint: you are free to introduce nontermination wherever.−kmicklas10yYou're correct that Idris doesn't force termination. That doesn't let you compute non-computable functions though (e.g. the busy beaver function).
Comments
From what I know, Idris does not have this constraint: you are free to introduce nontermination wherever.
You're correct that Idris doesn't force termination. That doesn't let you compute non-computable functions though (e.g. the busy beaver function).