3 ms·

I have found total checks in languages like idris helpful, but really only for catching small mistakes that I've made (for example, recursing on the original ar

• atennapel 6y ago
  If your language has equality proofs, for example `a = Int` then, if your language is non-total I can prove anything by divergence. So I can prove `Int = String`. This is still type-safe as long as you don't erase the proof, because you can never use the invalid proof because your program will diverge. So if you want to be type-safe but you still want to be able to erase proofs, your proofs have to be total.