Episode #125 of the Stack Overflow podcast is here. We talk Tilde Club and mechanical keyboards. Listen now

Note that the idea that a randomized algorithm as proof strategy, rather than a proof, is not unlike the idea that induction is a good proof strategy to show a universal quantification (over the natural numbers). This analogy may seem compelling, as induction is essentially the heart of recursion as a computational technique. (For any positive integer $$n$$, if you want to decide whether $$n^2$$ is a sum of the consecutive odd numbers preceding $$2n+1$$, you can reduce this to investigating whether $$(n-1)^2$$ is a sum of the consecutive odd numbers preceding $$2n-1$$, and so forth.) This is essentially an algorithmic proof-strategy which we have elevated to a theorem, allowing us to have the knowledge without explicitly computing it each time. However, induction is accepted constructively because it is already an axiom(-scheme) of Peano arithmetic; you can't prove it from the other axioms, whereas there is no rule of inference or axiom which allows the probabilistic method to prove existence constructively, or to constructively prove that probabilistic algorithms produce existence proofs, or anything along these lines. You simply cannot prove that there are examples of a class of object from the fact that there is a probabilistic algorithm to construct it, unless you already accept that proposition, either as an axiom, or from other premises.