We introduce a simple programming language for iteration-free probabilistic sequential programs and endow it with a complete and decidable Hoare calculus. In contrast to the usual approach, our state logic has truth-functional rather than arithmetical propositional connectives. Joint work with R. Chadha, P. Mateus and A. Sernadas.