> you mean that the _type systems_ of these languages are somewhat Turing-incomplete, not the languages themselves, right?
Either is a possibility.
Agda and Idris have full dependent types, that is every value computation is allowed to be used as a type parameter, so all value computations are forced to terminate in a way apparent to the typechecker and are consequently not Turing-complete. (As a sibling comment mentions, aside from hanging your compile when run an infinite loop is an example of empty so a proof of false, thus if the compiler decides it’s uninterested in the details and trusts it to work instead of actually running it it’s actually worse.)
ATS I think has a Turing-incomplete proof language distinct from the Turing-complete program language, but I’ve never been able to get through its rather arcane documentation so I’m not sure. Frama-C or SPARK is one example where I’m certain that’s the case (the program language is C or Ada, respectively), except the proof language is “throw intermediate statements at the SAT solver and see what sticks”.
Either is a possibility.
Agda and Idris have full dependent types, that is every value computation is allowed to be used as a type parameter, so all value computations are forced to terminate in a way apparent to the typechecker and are consequently not Turing-complete. (As a sibling comment mentions, aside from hanging your compile when run an infinite loop is an example of empty so a proof of false, thus if the compiler decides it’s uninterested in the details and trusts it to work instead of actually running it it’s actually worse.)
ATS I think has a Turing-incomplete proof language distinct from the Turing-complete program language, but I’ve never been able to get through its rather arcane documentation so I’m not sure. Frama-C or SPARK is one example where I’m certain that’s the case (the program language is C or Ada, respectively), except the proof language is “throw intermediate statements at the SAT solver and see what sticks”.