We present two semantic views of probabilistic programs and their relationship. An operational interpretation as well as a weakest precondition semantics are provided for an elementary probabilistic guarded command language. Our study treats features such as random sampling, conditioning, loop divergence, and non-determinism.

We then discuss two key analysis problems: almost-sure termination (does a program terminate with probability one?) and loop invariant synthesis.