Even if a world of quantum computing for everyone is years (if not decades) away, research on designing proper ways to program such systems has been ongoing for quite some time. History shows that programming is hard; making correct programs, that is, ones that conform to specifications, requires rigor and formal reasoning. Adapting the wide spectrum of formal techniques developed by the (classical) programming language community, from semantics to verification frameworks to proof assistants to the quantum paradigm, is thus key.

Ying’s work, which started years ago, focuses on defining a quantum Hoare-style logic approach to (quantum) program verification. This paper puts together a roadmap for the automatic verification of quantum programs written in a “while”-style idiom, extended to handle Hilbert-space states, unitary operators, and quantum variables. The agenda is actually pretty straightforward: follow all the traditional steps (syntax, operational, and denotational semantics; partial and total correctness; Hoare logic; proof techniques; invariants; mechanization) but with a quantum twist.

Readers need to be well versed in quantum computation notions (density operators, the Hadamard gate, entanglement, the controlled NOT gate (CNOT)) to really appreciate the results. However, even the uninitiated will get a feeling of the complexity induced by quantum specificities over traditional verification techniques. There is much more to be done (in this framework and in other competing approaches to quantum programming), so I would recommend this paper to programming language researchers interested in applying their knowledge to this new world.