[tobbebex]

Dependently typed languages such as Idris or Agda uses types for validation. Their type systems are also Turing complete, but you are only allowed to use total functions (that do halt) as proofs in types.