Résumé
The subtle semantics of probabilistic programs makes it difficult to correctly compile them. Moreover, because many inference algorithms for probabilistic programs are approximate and randomized, detecting miscompilation bugs is challenging. This talk describes work in progress developing a formally verified compiler for the Stan probabilistic programming language. The goal of verification is to produce a machine-checked proof of semantics preservation, meaning that the output of the compiler should have the same behavior as the original input program. The talk explains some of the novel challenges that arise in proving semantics preservation for a probabilistic programming language.
