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.
Extended abstract accepted for the poster session at PLanQC 2022 (co-located with ICFP 2022).