Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs

Charles Yuan | Chris McNally | Michael Carbin

Quantum programming languages enable developers to implement algorithms for quantum computers that promise computational breakthroughs in classically intractable tasks. Quantum programming requires awareness of entanglement, which can determine the correctness of algorithms and suitability of programming patterns.
In this work, we formalize purity as a central tool for automating reasoning about entanglement in quantum programs. A pure expression is one whose evaluation is unaffected by the measurement outcomes of qubits that it does not own, implying freedom from entanglement with any other expression in the computation.
We present Twist, the first language that features a type system for sound reasoning about purity. Twist enables the developer to identify pure expressions using type annotations. Twist also features purity assertion operators that state the absence of entanglement in the output of quantum gates. To soundly check these assertions, Twist uses a combination of static analysis and runtime verification.
We evaluate Twist’s design on a suite of quantum programs in simulation, demonstrating that Twist can express quantum algorithms, catch programming errors, and support programs that existing languages disallow, while incurring overhead of less than 3.5%.

Funding Sources: MIT-IBM Watson AI Lab | Intel Probabilistic Computing Center | Sloan Foundation