New Asst. Prof. Robert Rand Writes the Language of Tomorrow’s Quantum Computers
The age of quantum computers is fast approaching. Right now, companies large and small are engaged in a race to produce the first practical-scale quantum machines capable of performing calculations that would stump a classical computer, which will open new horizons in physics, cybersecurity, drug development, and other fields. Theoretical computer scientists have already designed some of the algorithms that these machines will be asked to run, but an important missing piece remains: what language will we speak to direct these quantum computers?
Robert Rand, who joined University of Chicago Computer Science this fall as an assistant professor, is part of the small but growing community of researchers creating quantum programming languages. Today’s programmers of classical computers have a vast library of languages they can use, from high-level languages such as Python and Java to more targeted languages for specific tasks such as working with databases or spreadsheets. But quantum computing languages sit closer to the early, pre-Fortran days of computer science, where many options exist but no consensus has emerged.
In his PhD work at the University of Pennsylvania and a postdoctoral fellowship with the University of Maryland and the Joint Center for Quantum Information and Computer Science, Rand and his collaborators created the language QWIRE and the compiler VOQC, two important steps for quantum programming. These open-source tools help programmers write code for quantum computers that is verifiable and optimized, critical qualities for the early steps into an entirely new computing paradigm.
It’s a problem that bridges both the theory and the practice of computing, Rand said, where programming languages serve as the interface that makes working with quantum machines possible.
“Quantum computing is just conceptually more difficult than regular computing,” Rand said. “You can think of regular computing as a game of billiards, where everything is generally deterministic: you can predict which way the balls are going to move around the table. Whereas in quantum computing, you have thousands of half- or quarter-billiard balls floating around, and none of them occupy a set spot on the table due to the principle of superposition. So one real challenge we have is trying to figure out the correct kind of abstractions for quantum computing and translating those into actual programming languages.”
Rand studied mathematics as an undergraduate and began his PhD studies in machine learning, but soon defected to Steve Zdancewic’s programming languages group. A couple of years in, Rand and fellow student Jennifer Paykin were given the opportunity to dig into the world of quantum computing, tasked with developing a mathematically-grounded quantum programming language in the style of the trailblazing Quipper language.
The project resulted in QWIRE, which among other advances enabled formal verification of its programs. Formal verification mathematically proves that an algorithm does what it aims to do without error, an important guarantee for programs where the consequences of failure are large, such as the code that underlies security protocols, hardware performance, or air transportation. But in quantum computing, formal verification can address an even more fundamental issue: how do you debug a program that you can’t even look at?
“There’s an observer effect that causes quantum states to collapse on themselves, and you suddenly find yourself in a tricky situation, where even if you carefully designed your program, how do you know your code is doing what it’s supposed to do?” Rand said. “Formal verification is a powerful approach to software assurance, extracting mathematical statements from your programs so that you can prove their correctness. Quantum computing right now is so closely tied to mathematics that the ability to go back and forth between programming and mathematical analysis is immensely valuable.”
The QWIRE project also led to the development, with Kesha Hietala and UMD collaborators, of VOQC, a quantum compiler that translates and optimizes code written in SQIR, an intermediate representation for quantum programs. Like the CompCert project that inspired it, VOQC guarantees that the optimized programs produced are always functionally identical to the original programs. VOQC also offers an open-source alternative to the proprietary compilers developed by members of the quantum computing industry, and is being used by researchers at Oak Ridge National Laboratory, among others.
Rand has channeled many of the findings of these projects into another effort: his online, interactive textbook, Verified Quantum Computing, which he plans to use in teaching at UChicago. The book takes a mathematical approach to its topic, teaching concepts by asking students to prove theorems, which can then be verified by an automated proof assistant.
“Writing a computer-checked proof sometimes feels like trying to convince a very small child that something is true, and that’s a great way to learn things,” Rand said. “The technology to do this kind of stuff is pretty new, and it's getting better all the time. This is my vision for the future, not just for quantum computing, but for learning in general: to tackle problems at the edge of your understanding and receive instant feedback.”
Rand will teach from his textbook at UChicago in a future advanced formal verification course, and will also lead courses on discrete mathematics and proof assistants. He’ll continue to play an active role in growing the global quantum programming community through meetings such as PLanQC, which he co-organized in 2020 and will again for 2021. And in Rand’s research, he will link up with Professor Fred Chong’s group and the EPiQC expedition, and collaborate with researchers at the Chicago Quantum Exchange and Argonne National Laboratory.
“UChicago's quantum computing group is unique in that it's not just a bunch of physicists or a bunch of theorists; those are the two groups of people who have traditionally been working on quantum computing,” Rand said. “Fred's group is very much trying to bridge that gap, using techniques from computer science to make quantum computing a reality a lot faster. My work on compilers and languages can be a big part of this effort: let's shrink that gap down. Let's make it so that we can execute these algorithms on real machines.”
