[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.