All programs need to be verified--even post-quantum cryptography software. To prove properties of such protocols requires proofs that involve not only quantum programming, but also pairs of programs, an encryptor and an attacker. But proof also implies that there is logic in which to do them.

The paper tries to do just this, leveraging recent work on probabilistic relational Hoare logic. A long introduction tries quite hard to give the intuition behind the work, suitable for researchers in programming languages, without assuming much knowledge of quantum computing or post-quantum cryptography, but assuming familiarity with Hoare logic(s) and what is needed for implementing programming language meta-theory atop an interactive theorem prover.

Then the paper proceeds with the very intricate, deeply technical developments needed to establish this new logic and its useful properties. Some examples are also worked out, but even these are very technical and very challenging. The author (very) frequently refers to additional material available in “the long version of this paper” (even though the paper at hand is 31 pages itself).

This work straddles so many different fields; it is remarkable that suitable, competent referees were found. A handful of experts will appreciate this work, but it will take a long time for the wider community to digest it.