[zozbot234]

AIUI, the fact that well-founded recursion is encoded as "noncomputable" in Lean is just a wart/quirk of that particular system; it can be justified in dependent type theory which is quite constructive and used by other systems such as Coq.

[kmill]

It's not `noncomputable` in Lean though. Lots of computable functions use it.

I've read Bauer's paper before btw. I think topoi are cool, but I don't think it's a complexity worth thinking about for everyone else who isn't concerned about these things.