  The "correct by construction" paradigm is an important component of modern
Formal Methods, and here we use the probabilistic Guarded-Command Language
$\mathit{pGCL}$ to illustrate its application to $\mathit{probabilistic}$
programming. $\mathit{pGCL}$ extends Dijkstra's guarded-command language
$\mathit{GCL}$ with probabilistic choice, and is equipped with a
correctness-preserving refinement relation $(\sqsubseteq)$ that enables
compact, abstract specifications of probabilistic properties to be transformed
gradually to concrete, executable code by applying mathematical insights in a
systematic and layered way. Characteristically for "correctness by
construction", as far as possible the reasoning in each refinement-step layer
does not depend on earlier layers, and does not affect later ones. We
demonstrate the technique by deriving a fair-coin implementation of any given
discrete probability distribution. In the special case of simulating a fair
die, our correct-by-construction algorithm turns out to be "within spitting
distance" of Knuth and Yao's optimal solution.
