[ori_b]

How are you finding Idris? or are you more in the Agda camp?

If you want to definitely rule out as many errors as possible, dependently typed languages are the state of the art, allowing you to write a sort function that will fail to compile if it returns a list that isn't sorted (eg,https://dafoster.net/articles/2015/02/27/proof-terms-in-idri..., or https://www.twanvl.nl/blog/agda/sorting).

After all, if you can't even prove basic properties about your code from your language, like array accesses being within bounds, are you really using all possible tools to rule out errors at your disposal?

[choeger]

To be fair, I never had a chance to use Idris nor Agda. I don't know how capable I would be to encode the proofs in libraries nor client code. If it's usable, I am all for it.

Otoh, I do know that languages like OCaml, Haskell, or Rust take the burden of trivial errors from my shoulders for neglible cost.

[eyelidlessness]

Yeah, that was an insincere gotcha question, and it's a shame that it could potentially undermine other readers' potential value of a higher degree of confidence versus a hypothetically perfect confidence.