This paper presents a theory of probabilistic programming based on relational calculus through a series of stages; each stage concentrates on a different and smaller class of program, defined by the healthiness conditions of increasing strength. At each stage we show that the notation of the probabilistic language conserve the healthiness conditions of their operands, and that every theory conserves the definition of recursion.