The extensive deployment of probabilistic algorithms has radically changed our perspective on several well-established computational notions. Correctness is probably the most basic one. While a typical probabilistic program cannot be said to compute the correct result, we often have quite strong expectations about the frequency with which it should return certain outputs. In these cases, trust as a generalisation of correctness fares better. One way to understand it is to say that a probabilistic computational process is trustworthy if the frequency of its outputs is compliant with a probability distribution which models its expected behaviour. We present a formal computational framework that formalises this idea. In order to do so, we define a typed lambda-calculus that features operators for conducting experiments at runtime on probabilistic programs and for evaluating whether they compute outputs as determined by a target probability distribution. After proving some fundamental computational properties of the calculus, such as progress and termination, we define a static notion of confidence that allows to prove that our notion of trust behaves correctly with respect to the basic tenets of probability theory.

翻译：概率算法的大规模部署从根本上改变了我们对若干成熟计算概念的认知。正确性可能是其中最基本的概念。虽然通常无法断言一个典型的概率程序能计算出正确结果，但我们往往对其返回特定输出的频率抱有相当强的期望。在这种情况下，作为正确性概念的推广，"信任"这一概念更为适用。理解信任的一种方式是：若概率计算过程的输出频率符合刻画其预期行为的概率分布，则该过程值得信赖。本文提出一个形式化的计算框架来阐明这一思想。具体而言，我们定义了一个类型化λ-演算，该演算包含可在运行时对概率程序进行实验的算子，以及用于评估程序输出是否符合目标概率分布的算子。在证明了该演算的基本计算性质（如进展性、终止性）之后，我们定义了一种静态置信度概念，从而能够证明我们的信任概念与概率论基本原理具有行为一致性。