Yep, but one could express a computable predicate classically (e.g. by unnecessarily invoking the axiom of choice in its definition). Using a constructive proof

Yep, but one could express a computable predicate classically (e.g. by unnecessarily invoking the axiom of choice in its definition). Using a constructive proof assistant prevents accidentally doing this, and encourages using constructive definitions where possible. It also encourages using computable mathematical formulations (e.g. computable reals vs classical reals).