Existing inference methods for probabilistic program are either stochastic (e.g. MCMC, SVI) or exact (e.g. using computer algebra). Stochastic methods may converge slowly, which can be difficult to detect. Exact inference, on the other hand, requires restrictions on the class of supported programs, such as disallowing recursion. We propose to approximate the posterior not in a stochastic way, but to compute rigorous bounds on the posterior. To achieve this for general probabilistic programs, allowing recursion, we use a semantics based on interval traces and interval arithmetic, together with a type and constraint system. We have proved soundness and (under mild conditions) completeness of our approach. Our prototype implementation gives promising results that allow us to recognize wrong inference results.