Quantum computing (QC) represents the future of computing systems, but the tools for reasoning about the quantum model of computation, in which the laws obeyed are those on the quantum mechanical scale, are still a mix of linear algebra and Dirac notation; two subjects more suitable for physicists, rather than computer scientists and software engineers. On this ground, we believe it is possible to provide a more intuitive approach to thinking and writing about quantum computing systems, in order to simplify the design of quantum algorithms and the development of quantum software. In this paper, we move the first step in such direction, introducing a specification language as the tool to represent the operations of a quantum computer via axiomatic definitions, by adopting the same symbolisms and reasoning principles used by formal methods in software engineering. We name this approach formal quantum software engineering (F-QSE). This work assumes familiarity with the basic principles of quantum mechanics (QM), with the use of Zed (Z) which is a formal language of software engineering (SE), and with the notation and techniques of first-order logic (FOL) and functional programming (FP).
Quantum computing (QC) represents the future of computing systems, but the tools for reasoning about the quantum model of computation, in which the laws obeyed are those on the quantum mechanical scale, are still a mix of linear algebra and Dirac notation; two subjects more suitable for physicists, rather than computer scientists and software engineers. On this ground, we believe it is possible to provide a more intuitive approach to thinking and writing about quantum computing systems, in order to simplify the design of quantum algorithms and the development of quantum software. In this paper, we move the first step in such direction, introducing a specification language as the tool to represent the operations of a quantum computer via axiomatic definitions, by adopting the same symbolisms and reasoning principles used by formal methods in software engineering. We name this approach formal quantum software engineering (F-QSE). This work assumes familiarity with the basic principles of quantum mechanics (QM), with the use of Zed (Z) which is a formal language of software engineering (SE), and with the notation and techniques of first-order logic (FOL) and functional programming (FP).
Recent progress in quantum computing has under-scored the need for specialized software to effectively address the unique challenges posed by quantum systems. While early research emphasized hardware and algorithmic breakthroughs, recent progress underscores the necessity of Quantum Soft-ware Engineering (QSE), an emerging discipline that combines software lifecycle processes, tooling, hybrid orchestration, and human-centered design. This paper integrates insights from QSE and quantum software architecture (QSA) to propose a hybrid execution architecture explicitly shaped by Quantum HCI principles, emphasizing developer experience, trust, and the quality of interaction with quantum systems. While quantum software represents a new genre of software-intensive systems, existing processes and notations can be adapted to derive architecting activities and develop modeling languages for quantum software. Additionally, tool chains can incorporate reusable knowledge and roles to automate and customize the architectural process. By analyzing current research and iden-tifying existing gaps, this paper aims to guide the systematic development of robust and scalable quantum software systems. Central to this vision is meaningful human interaction, ensuring that developers can interpret, act on, and trust system outputs from design to post-execution analysis.
There are no doubts that quantum programming and, in general, quantum computing, is one of the most promising areas within computer science and one of the areas where most expectations are being placed in recent years. Although the days when reliable and affordable quantum computers will be available is still a long way off, the explosion of programming languages for quantum programming has grown exponentially in recent years. The software engineering community has been quick to react to the need to adopt and adapt well-known tools and methods for software development, and for the design of new ones tailored to this new programming paradigm. However, many key aspects for its success depend on the establishment of an appropriate conceptual framework for the conception and design of quantum programs. This article discusses the concept of module, key in the software engineering discipline, and establishes initial criteria for determining the cohesion and coupling levels of a module in the field of quantum programming as a first step towards a sound quantum software engineering. As detailed in the article, the conceptual differences between classical and quantum computing are so pronounced that the translation of classical concepts to the new programming approach is not straightforward.
The field of quantum mechanics predates computer science by at least ten years, the time between the publication of the Schrodinger equation and the Church-Turing thesis. It took another fifty years for Feynman to recognize that harnessing quantum mechanics is necessary to efficiently simulate physics and for David Deutsch to propose the quantum Turing machine. After thirty more years, we are finally getting close to the first general-purpose quantum computers based upon prototypes by IBM, Intel, Google and others.\nWhile physicists and engineers have worked on building scalable quantum computers, theoretical computer scientists have made their own advances. Complexity theorists introduced quantum complexity classes like BQP and QMA; Shor and Grover developed their famous algorithms for factoring and unstructured search. Programming languages researchers pursued two main research directions: Small-scale languages like QPL and the quantum lambda-calculi for reasoning about quantum computation and large-scale languages like Quipper and Q# for industrial-scale quantum software development. This thesis aims to unify these two threads while adding a third one: formal verification.\nWe argue that quantum programs demand machine-checkable proofs of correctness. We justify this on the basis of the complexity of programs manipulating quantum states, the expense of running quantum programs, and the inapplicability of traditional debugging techniques to programs whose states cannot be examined. We further argue that the existing mathematical models of quantum computation make this an easier task than one could reasonably expect. In light of these observations we introduce QWIRE, a tool for writing verifiable, large scale quantum programs.\nQWIRE is not merely a language for writing and verifying quantum circuits: it is a verified circuit description language. This means that the semantics of QWIRE circuits are verified in the Coq proof assistant. We also implement verified abstractions, like ancilla management and reversible circuit compilation. Finally, we turn QWIRE and Coq's abilities outwards, towards verifying popular quantum algorithms like quantum teleportation. We argue that this tool provides a solid foundation for research into quantum programming languages and formal verification going forward.
Quantum computing is rapidly transitioning from a scientific curiosity to an industrial reality, offering the potential to overcome classical computation limitations. This shift has given rise to the field of quantum software engineering (QSE), focused on developing novel approaches for engineering large-scale quantum applications. Traditional software engineering methods fall short in addressing the unique characteristics of quantum computing, necessitating innovative QSE methodologies and tools. While progress has been made in testing and debugging quantum programs, very little work has been done on analyzing if and how existing requirements engineering techniques can address the challenges that designing quantum software raises. This paper discusses some of the challenges for requirements engineers while eliciting requirements for quantum software, modeling the collected requirements, and analyzing them, and introduces some initial solutions for eliciting, modeling, and analyzing quantum requirements.
As quantum computing continues to advance, the development of reliable and scalable quantum software systems becomes increasingly crucial. However, designing and implementing hybrid (quantum-classical) software systems poses unique challenges that require novel approaches and best practices. This position paper argues for the importance of developing architectural and design patterns specific to Quantum Software Engineering (QSE). We provide an overview of existing quantum software design patterns (more focused on low-level, programming details) and highlight the lack of patterns addressing hybrid software systems and architectural patterns. We discuss the key challenges that architectural patterns should address, including quantum-classical integration, maintainability, efficiency, and security. We also discuss the implications for practitioners, providing guidance on how to think high-level about hybrid software development process. Finally, we outline future research directions and emphasize the need for collaboration between the quantum computing and software engineering communities to establish a comprehensive high-level patterns framework for QSE.
Quantum systems have started to emerge as a disruptive technology and enabling platforms - exploiting the principles of quantum mechanics - to achieve quantum supremacy in computing. Academic research, industrial projects (e.g., Amazon Braket), and consortiums like 'Quantum Flagship' are striving to develop practically capable and commercially viable quantum computing (QC) systems and technologies. Quantum Computing as a Service (QCaaS) is viewed as a solution attuned to the philosophy of service-orientation that can offer QC resources and platforms, as utility computing, to individuals and organisations who do not own quantum computers. To understand the quantum service development life cycle and pinpoint emerging trends, we used evidence-based software engineering approach to conduct a systematic mapping study (SMS) of research that enables or enhances QCaaS. The SMS process retrieved a total of 55 studies, and based on their qualitative assessment we selected 9 of them to investigate (i) the functional aspects, design models, patterns, programming languages, deployment platforms, and (ii) trends of emerging research on QCaaS. The results indicate three modelling notations and a catalogue of five design patterns to architect QCaaS, whereas Python (native code or frameworks) and Amazon Braket are the predominant solutions to implement and deploy QCaaS solutions. From the quantum software engineering (QSE) perspective, this SMS provides empirically grounded findings that could help derive processes, patterns, and reference architectures to engineer software services for QC.