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