3 ms·
Idris is an other example for a programming language that always terminates. For that matter any total functional programming language does and is therefore tur
by vbrandl 6y ago
Idris is an other example for a programming language that always terminates. For that matter any total functional programming language does and is therefore turing incomplete.
- dddbbb 6y agoTotality is optional in Idris. Also, the big dependently-typed languages like Coq, Agda, Idris all support corecursion, so they can run programs infinitely provided the program does something productive.