Beyond Separation: Toward a Specification Language for Modular Reasoning about Quantum Programs


There has been a recent surge of interest in separation logics for quantum computation. Unlike Reynolds’ initial attempts to formulate a separation logic for reasoning about pointer manipulation using small, intuitive programs, the attempts in the quantum setting have been to provide precise formulations of theory without providing much intuition. We argue that these attempts may be misguided: the fundamental problem hindering scalability of Hoare-like logics is modular reasoning about entangled, rather than separable, states. Hiding behind all their formal complexity, current logics are either too restrictive or, at best, solve simplistic problems. We motivate the quantum program verification community by proposing an ideal specification language.

The Third International Workshop on Programming Languages for Quantum Computing 2022: Poster

Extended abstract accepted for the poster session at PLanQC 2022 (co-located with ICFP 2022).