alt Hacker News> 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.
That's not true. Non-constructive logics are extensions of constructive logics. You can express any algorithm in TLA+, and much more than algorithms.
You are right that when using non constructive logics, it's not guaranteed that the proof is executable as a program, but that's not a downside. Having the proof be a program in some sense is interesting, but it's not particularly useful.