Totality checking like that in Idris is one nice example. That's kind of circular though - it isn't Turing complete because it has totality checking (i.e. you m

Totality checking like that in Idris is one nice example. That's kind of circular though - it isn't Turing complete because it has totality checking (i.e. you must prove the program terminates).