Comment on Idris, a language that will change the way you think about programming (2015)parentComments−dllthomas10yAlmost arbitrarily - they must be computable... ;)−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
Almost arbitrarily - they must be computable... ;)
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).