That's not how constructivity works, though --- it's all or nothing. You can be careful about the points at which you use classical reasoning (or, here, probab

That's not how constructivity works, though --- it's all or nothing. You can be careful about the points at which you use classical reasoning (or, here, probability), but then the whole proof is no longer constructive. The argument in favor of the constructive approach is that you can very carefully decide when you depart from it. For a (Curry-Howard) corresponding intuition, a program is no longer functional the moment any computational effect is involved (mutable state, control effects like continuations and backtracking, etc.).