Posts -

Taking my home work setup seriously

Ergonomics & settling in for the long haul

Posted on August 14, 2020 (Last modified on January 23, 2022) | Andrew Helwer

The headlines don’t lie. Microsoft, Google, Amazon, Facebook, and a whole host of other tech companies have announced employees will be working from home until early-mid 2021. There are reasons to believe this will be pushed back; even if the staggeringly ambitious timelines for vaccine development are met, a vaccine might not be a silver bullet and the pandemic could require management for the next 2-3 years. As a software engineer in big tech’s orbit, this means it’s time to settle in for the long haul and take my home work setup seriously. [Read More]

practices

Doing a math assignment with the Lean theorem prover

Posted on April 5, 2020 | Andrew Helwer

Turn back the clock to 2009: a confused physics major newly infatuated with math and computer science, I enrolled in MATH 273: Numbers and Proofs at the University of Calgary. This wasn’t my first encounter with mathematical proof; in first-year calculus I’d mastered rote regurgitation of delta-epsilon proofs. Despite writing out several dozen, their meaning never progressed beyond a sort of incantation I can summon to this day (for every \( \epsilon > 0 \) there exists a \( \delta > 0 \) such that…). [Read More]

formal methods

Simulating physical reality with a quantum computer

Quantum chemistry for complete beginners

Posted on December 21, 2019 | 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. [Read More]

quantum computing

Walking the faster-than-light tightrope

Quantum entanglement and the CHSH game

Posted on December 7, 2018 | Andrew Helwer

Measurement and signaling in the nonlocal world Popular understanding of quantum mechanics usually focuses on three learning objectives: 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. 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. [Read More]

quantum computing

Checking Firewall Equivalence with Z3

Posted on February 13, 2018 | Andrew Helwer

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. [Read More]

formal methods smt solvers

Formal Verification, Casually Explained

Written during an interesting time in my life

Posted on February 12, 2018 | Andrew Helwer

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. [Read More]

formal methods philosophy