Title seems a little misleading, in that some constructive proof techniques are used to set-up the probabilistic tools.
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.).