> in surfacing computational content, which is the whole point of constructive proof

The point of a constructive proof is that the proof itself is in some way computational [1], not that the algorithm is. When I wrote formal proofs, I used either TLA+ or Isabelle/HOL, neither of which are constructive. It's easy to describe the notion of "constructive computation" in a non-constructive logic without any additional effort (that's because non-constructive logics are a superset of constructive logics; i.e. they strictly admit more theorems).

[1]: Disregarding computational complexity

> When I wrote formal proofs, I used either TLA+ or Isabelle/HOL, neither of which are constructive.

True, but this requires using different formal systems for the algorithm and the proof. Isabelle/HOL being non-constructive means you can't fully express proof-carrying code in that single system, without tacking on something else for the "purely computational" added content.