Sampling languages: Semantics and verification of sampling-based inference algorithms for probabilistic programming