Independent software engineering consultant with over a decade of professional experience.
Previously worked at Acceleware, Microsoft Azure Compute, Microsoft Azure Networking, and Microsoft Quantum.
BSc in Computer Science from the University of Calgary.
From Canada, currently based out of Atlanta, GA, USA.
TLA⁺ enthusiast!
Republished from Teleport’s official blog (link). I received compensation from Teleport for writing this post.
Z3 is a satisfiability modulo theories (SMT) solver developed by Microsoft Research. With a description like that you’d expect it to be restricted to esoteric corners of the computerized mathematics world, but it’s made impressive inroads addressing conventional software engineering needs: analyzing network ACLs and firewalls in Microsoft Azure, for example. Z3 is used to answer otherwise-unanswerable questions like “are these two firewalls equivalent?
[Read More]
Interpretations of quantum mechanics are boring. Boring! Maybe the universe has a strict partition between quantum and non-quantum. Maybe there are a bunch of parallel universes with limited crosstalk. Or maybe it’s whatever the Bohmian mechanics people are talking about. Shut up and calculate, I think. I don’t say this out of some disdain for idle philosophizing or to put on airs of a salt-of-the-earth laborer in the equation mines. It’s just there are so, so many interesting things you can learn about in quantum theory without ever going near the interpretation question.
[Read More]
In which I am stunted upon by coin flips Wasn’t too long ago that I felt pretty good about my knowledge of distributed systems. All someone really needed in order to understand them, I thought, was a thorough understanding of the paxos protocol and a willingness to reshape your brain in the image of TLA⁺. Maybe add a dash of conflict-free replicated datatypes, just so you know what “eventual consistency” means.
[Read More]
This isn’t going to be a post about how adopting a several-thousand-year-old practice can make you a better servant of capital. Instead, let’s talk about when I feel the lowest of the low. It comes after spending any number of hours on my computer, maybe even a full day, endlessly circling around different websites in search of stimulation, the quick jolt that comes with learning an interesting fact or watching a funny short video or seeing someone get dunked on for having a bad political opinion.
[Read More]
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]
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]
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]
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]
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]
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]
