4 ms·

You probably could, but part of the purpose of Idris is to statically prove things with dependent types rather than test them.

• chriswarbo 9y ago
  Testing and proving aren't mutually exclusive; there's also a more fine-grained distinction, between proving things (say, with pen and paper, or an SMT solver, or whatever) and proving things using the type system of the language they're implemented in. The nice thing about Idris is that it's specifically created with such "practical" issues in mind: it gives you powerful tools, but there's absolutely no obligation to use them. If you want to, you can avoid checking certain (or all) parts of a program. You need to define enough types to represent your computation/data, but not to prove its correctness; e.g. you can over-represent your domain using a bunch of sum types, stick infinite loops in the branches you know/think are unreachable, then turn off totality checking. If we compare this to, say, Coq or Agda, not only must you prove everything-you-write-in-those-languages, you must also prove everything-you-write in those languages! (i.e. everything you write must be proved, and only proofs written in Coq/Agda will be accepted). You can assert axioms, but not their computational/runtime meaning, which is problematic when using them as a programming language.