GOALS

Recent years have seen the emergence of a number of research groups that aim to advance quantum computing and to develop a skilled quantum software workforce. A particular challenge that must be overcome for safe quantum computing at scale is the creation of robust, expressive, efficient, and tractable formal verification tools. Since there is currently no event dedicated to this pursuit, the first goal of this Dagstuhl Seminar is to bring together a dedicated community of researchers in a single venue. This will give participants an opportunity to identify and discuss the most pressing challenges and promising directions for quantum programming and verification.

The second goal of this seminar is to develop connections with neighboring fields. In its effort to create tools and foundations for verified quantum programming, the emerging quantum software community will benefit from paying careful attention to adjacent work, in quantum hardware engineering, development of quantum algorithms, and target applications.

Finally, we see this Dagstuhl Seminar as an opportunity to take a general snapshot of the field as it currently exists. It should synthesize the state of the art of quantum software science, such as current leading solutions in programming, benchmarking of existing tools for verification and optimization, software testing, and error-correction.

TOPICS

The problem of debugging and verification. Although quantum computing holds great promise, the correct implementation of quantum algorithms is still a challenging problem. Reasoning about quantum programs in the standard Hilbert space formalism requires formalizing low-level statements about complex numbers, matrices, and other linear algebraic concepts, which is far from the level of abstraction at which quantum algorithms are usually specified in the research literature. This makes it difficult not just to verify quantum programs, but even to formally specify their intended behavior. It also makes it hard to write correct programs in the first place. Furthermore, due to the specific laws of quantum physics – destructive measurement and nondeterminism – standard debugging methods fail in the quantum case. As a result, formal methods and static analysis are likely to play a decisive role in future quantum software engineering, at every stage of the development process (high-level languages, compilation, code optimization, error-correction, architecture mapping, etc.). New research challenges include developing appropriate symbolic representations, specification languages, and proof engines. An alternative strategy for ensuring reliability of quantum programs relies on classical simulation, with converging efforts toward symbolic execution and tensor network approximations techniques.

Quantum programming languages. Many current environments for quantum programming tend to focus on the description of sequences of elementary quantum operations, analogous to assembly code in the classical setting. However, to realize the true potential of quantum computing, it will be necessary to program large-scale error-corrected quantum computers, possibly integrated in a larger computing architecture involving hybrid computations. To achieve reliable computations at this scale, it will be necessary to develop high-level quantum programming languages with appropriate abstractions and intuitive features on the foundation of a well-developed theory.

Guaranteed compilation. Any future deployment of quantum computing on a practical scale will also require a major effort in quantum compilation. Developing optimized, practical and reliable quantum software stacks requires a significant research effort. It involves the development of dedicated algorithms and theories aimed at achieving various optimization goals, evaluation metrics, and tools, together with relative correctness guarantees.

Hardware agnosticism. One special consideration for quantum computing is the diversity of quantum computing models. It includes gate-based calculus, measurement-based quantum computing, adiabatic computation, photonic quantum computation, and Hamiltonian simulation. This raises a number of software engineering problems, such as: Can we develop abstractions, formalizations and reasoning methods transcending this hardware diversity? Can we think about a generic quantum programming language, agnostic of the target computing model and architecture? How can software bridge multiple modes of quantum computation, often within single systems?

Creative Commons BY 4.0

Christophe Chareton, Yu-Fang Chen, Robert Rand, and Peter Selinger