Andrew Helwer

Quantum Computers: Not Just for Breaking RSA

There’s no denying it, Shor’s algorithm was a blockbuster result. The thought of an exotic new computer breaking all widely-used public-key crypto plays well with the public imagination, and so you’d be forgiven for believing quantum computing is ultimately a sort of billions-dollar make-work project for software engineers: forcing our profession to relive a Y2K-like mass upgrade of old systems to new, quantum-safe encryption algorithms. Great for consultants, bad for people who want resources invested toward actual social good.

Measurement and signaling in the nonlocal world

Popular understanding of quantum mechanics usually focuses on three learning objectives:

1. At small scales, particle properties (position, momentum, spin, etc.) are in superposition - they don’t have a definite value, but instead are “smeared” across multiple possible values.
2. Measuring a superposed particle property makes it collapse probabilistically to a specific value. We don’t simply discover the property’s pre-existing value; rather the property is forced to take on a definite value by the act of measurement.
3. Particles can be entangled, which means operations on one affect the other instantaneously across arbitrarily-large distances (known as nonlocality); however, this has restrictions and cannot be used for faster-than-light (FTL) communication.

Lessons I’ve learned from software engineering are uniformly cynical:

• Abstraction almost always fails; you can’t build something on top of a system without understanding how that system works.
• Bleeding-edge methods are a recipe for disaster
• Everything good is hype and you’ll only ever get a small fraction of the utility being promised.

Imagine my surprise, then, when the Z3 constraint solver from Microsoft Research effortlessly dispatched the thorniest technical problem I’ve been given in my short professional career.

Why are we here?

What guarantees does formal verification provide? This question rests at the apex of a hierarchy of inquiry extending all the way down to how we can know anything at all!

What do we mean by software correctness?

There are precisely two different ways for a piece of software to be correct:

• The supreme deity of the universe descends from the heavens and decrees, with all the weight of Objective Truth, that a certain piece of software is correct.
• We have a list of things we want the software to do, and use logic to prove the software does these things.

Crafty readers will come up with, like, twenty different caveats to the second definition. I encourage it! Take a minute to unearth some of the hidden assumptions. Good? Good. I’ll talk about those hidden assumptions in greater detail below, but the point I want to make is this: there is no such thing as inherently correct software. Your wacky program could say 1 * 1 = 2, and that isn’t incorrect in any objective sense - if that’s how you want your program to behave, heck, knock yourself out. We call our list of things we want the software to do a specification. A program is only correct (or incorrect) relative to its specification; if the program is correct relative to its specification, we say it implements or refines the specification.