undefined | Better HN

0 pointschoeger4y ago0 comments

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.

0 comments

eyelidlessness4y ago

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.

j / k navigate · click thread line to collapse

0 pointschoeger4y ago0 comments

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.

0 comments

eyelidlessness4y ago

j / k navigate · click thread line to collapse