> while a classical mathematician will forever be tormented by the existence of theorems they cannot prove in their chosen formalism.
As a devotee to the law of excluded middle myself, I don't feel particularly tormented by this.
(I agree with your wider point that constructivism isn't the root cause of independent statements in mathematical foundation theories.)