The notion of approximate equivalence of programs plays a fundamental role in several fields of computer science. In particular one way of tackling this when dealing with probabilistic programs is to consider the statistical distance (SD) between memory distributions. Despite the SD being a well-known concept from measure theory, all the treatment it has received in the computer science literature to model and reason about approximate equivalence of programs has been very poor and deficient.

In this talk I will present an ongoing work that attempts to fill this gap. First I will show a SD-based extension of a relational Hoare logic for probabilistic programs proposed by Barthe et al that allows to reason about approximate observational equivalence. Second I will exhibit related results for two typical scenarios in the domain of cryptography: uptobad programs and the presence of adversaries of unknown code. To conclude, I will illustrate the benefits of this approach by showing how it allowed to formalize two case studies in the Certicrypt framework.