Recent developments in quantum hardware are raising hope that efficient quantum machines will be available in the near future. Software engineering approaches specific to quantum are thus needed.
Debugging and code verification are two major challenges. Classical approaches based on assertion testing and verification are simply incompatible with the laws of quantum physics (indeterminacy, the fact that measurement destroys quantum information, etc.) that underpin quantum computing. The CEA has built on its historic experience with classical code analysis and formal verification to create a new approach for quantum software.
Specifically, a quantum programming language and formal semantics are combined to:
This approach leverages the same deductive verification techniques proven on classical code. Quantum calculations are represented symbolically as sums of paths, a discrete version of Feynman’s path integral formulation (Figure 2).
Qbricks has been proven on the fully verified development of non-trivial quantum algorithms, including the first proven implementation of Shor’s algorithm, placing it at the international state of the art (Figure 3). A paper on the approach was presented at the European Symposium on Programming (ESOP) in 2021 and a book chapter was published in 2023.
The focus is now on integrating Qbricks into a complete and operational quantum software development chain and, specifically:
Qbricks solves the problem of how to safely and efficiently develop quantum software by adapting the best practices in classical software development (languages, code analysis, and compilation) to the specificities of quantum.
“We are developing formal verification tools for reliable development and compilation.
