As the scale and capability of quantum hardware improves, there is a growing need for more expressive languages and frameworks that enable developers to write, optimize, and debug quantum programs beyond low-level quantum circuits. Motivated by ongoing collaborative work [1], this talk will showcase the role of abstraction in quantum software development. The characteristics of “good” abstractions will be described, and their importance highlighted by the examples of building an interactive quantum debugger [2], and optimizing quantum programs at multiple levels. Determining the “right” set of abstractions is a challenging open question that requires further research.
As the scale and capability of quantum hardware improves, there is a growing need for more expressive languages and frameworks that enable developers to write, optimize, and debug quantum programs beyond low-level quantum circuits. Motivated by ongoing collaborative work [1], this talk will showcase the role of abstraction in quantum software development. The characteristics of “good” abstractions will be described, and their importance highlighted by the examples of building an interactive quantum debugger [2], and optimizing quantum programs at multiple levels. Determining the “right” set of abstractions is a challenging open question that requires further research.
Quantum programming languages provide necessary constructs to program quantum computers. To write such programs, one needs to understand the characteristics of quantum computers such as superposition and entanglement, which are novel as compared to programming with classical computers. Understanding these characteristics requires an understanding of quantum physics. Thus, there is a need to build high-level modeling abstractions of quantum programs for software engineers who are used to program on classical computers to understand and model quantum programs at a high-level of abstraction and independent of quantum platforms. To this end, we present some ideas for developing such quantum software modeling languages, by presenting a conceptual model of quantum programs and an example of modeling the state-based behavior of quantum entanglement program. Moreover, we present some open issues in the area of modeling quantum programs.
While recent progress in quantum hardware open the door for significant speedup in certain key areas (cryptography, biology, chemistry, optimization, machine learning, etc), quantum algorithms are still hard to implement right, and the validation of such quantum programs is achallenge. Moreover, importing the testing and debugging practices at use in classical programming is extremely difficult in the quantum case, due to the destructive aspect of quantum measurement. As an alternative strategy, formal methods are prone to play a decisive role in the emerging field of quantum software. Recent works initiate solutions for problems occurring at every stage of the development process: high-level program design, implementation, compilation, etc. We review the induced challenges for an efficient use of formal methods in quantum computing and the current most promising research directions.
The computer industry, with over seven decades of experience to draw on, has shown that to thrive, there must be a community of software engineers that produce the applications users depend on. Supporting those software engineers so they can write code that performs well across multiple generations of hardware (since application software generally lasts longer than hardware) is fundamental to sustaining the computer industry. Today's quantum software developers must reason at a low level, close to the hardware, which is not sustainable. In this paper, we assert that quantum computing needs high-level abstractions that support a quantum computing applications ecosystem. A single abstraction that bridges from the mental models used by a programmer to the details of how qubits are realized in hardware is unlikely to work. We need a hierarchy of tightly coupled models that define a framework for reasoning about the software development process in quantum computing. We propose an abstraction hierarchy and then explore its utility with two approaches to the eigenvalue estimation problem: (1) a variational algorithm with error mitigation, and (2) phase estimation with error correction. We use our proposed abstraction hierarchy to pinpoint key differences between these approaches and demonstrate how an abstraction hierarchy helps us understand software development. This supports our central conclusion; that it is not enough to understand individual components of a software stack. To make progress, we need to think about an abstraction hierarchy holistically.
In this talk, I will give an overview of some recent progress and current challenges in the design of quantum programming languages. Unlike classical programs, which can in principle be debugged by stopping the program at critical moments and examining the contents of variables, quantum programs are not amenable to traditional debugging because the state of a quantum system cannot usually be examined in a meaningful way. Therefore, we need other methods for ensuring the correctness of quantum programs, such as formal verification. For this reason, I advocate the use of strongly typed, functional programming languages for quantum computing. As far as functional quantum programming languages are concerned, there is currently a relatively wide gap between theory and practice. On the one hand, we have languages with strong theoretical foundations, such as the quantum lambda calculus, which operate at a relatively low level of abstraction and lack many features that would be useful to practical quantum programmers. On the other hand, we have practical functional quantum programming languages such as Quipper, which is implemented as an embedded language in Haskell, has many high-level features, and has been used in large-scale projects, but lacks a theoretical basis and a strong type system [Green et al., 2013; Green et al., 2013; Green et al., 2013; Smith et al., 2014]. We have recently attempted to narrow this gap through a family of languages called Proto-Quipper, which are designed to offer Quipper-like features while having sound theoretical foundations [Ross, 2015; Rios and Selinger, 2018]. I will give an overview of Quipper and its most useful features, report on the progress we made with formalizing fragments of Quipper, and outline several of the still remaining challenges.
Abstract As implementations of quantum computers grow in size and maturity, the question of how to program this new class of machines is attracting increasing attention in the software engineering domain. Yet, many questions from how to design expressible quantum languages augmented with formal semantics via implementing appropriate optimizing compilers to abstracting details of machine properties in software systems remain challenging. Performing research at this intersection of quantum computing and software engineering requires sufficient knowledge of the physical processes underlying quantum computations, and how to model these. In this chapter, we review a superoperator-based approach to quantum dynamics, as it can provide means that are sufficiently abstract, yet concrete enough to be useful in quantum software and systems engineering, and outline how it is used in several important applications in the field.
Recent advancements in quantum computing software are gradually increasing the scope and size of quantum programs being developed. At the same time, however, these larger programs provide more possibilities for functional errors that are harder to detect and resolve. Meanwhile, debugging tools that could aid developers in resolving these errors are still barely existent and far from what we take for granted in classical design automation and software engineering. As a result, even if one manages to identify the incorrect behavior of a developed quantum program, detecting and resolving the underlying errors in the program remains a time-consuming and tedious task. Moreover, the exponential growth of the state space in quantum programs makes the efficient manual investigation of errors radically difficult even for respectively simple algorithms, and almost impossible as the number of qubits increases. To address this problem, this work proposes a debugging framework, available as an open-source implementation at https://github.com/cda-tum/mqt-debugger. It assists developers in debugging errors in quantum programs, allowing them to efficiently identify the existence of errors and diagnose their causes. Users are given the ability to place assertions in the code that test for the correctness of a given algorithm and are evaluated using classical simulations of the underlying quantum program. Once an assertion fails, the proposed framework employs different diagnostic methods to point towards possible error causes. This way, the debugging workload for quantum programs is drastically reduced.