Trip Report: Buck Mountain

Entiat Mountains, Central Cascades, WA, USA

Republished from the WTA website here. Climbed Buck Mountain via High Pass route, a long winding 16-ish mile approach with some incredible views. Main takeaways: Hiking boots probably fine Never needed ice axe or traction Many water sources along trail Parts of the trail were indistinguishable from the enchantments, with light-colored granite slabs towering over pristine alpine lakes. Great views of Glacier Peak, Clark Mountain (with the Walrus Glacier! [Read More]

Walking the faster-than-light tightrope

Quantum entanglement and the CHSH game

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]

Checking Firewall Equivalence with Z3

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 Verification, Casually Explained

Written during an interesting time in my life

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]

Trip Report: Hidden Lake Lookout

North Cascades, WA, USA

Republished from the WTA website here. Summary A very rough road leads to the trailhead. No parking or camping permits required. There is a long middle section with switchbacks through thorny plants without any shade. Water sources are plentiful. Horseflies were annoying. Many flat sites are available for camping, but beware one in an active rockfall area. Snow is easily traversible without microspikes or even trekking poles. There is only one latrine on the entire mountain, which is only easily accessible from the lookout. [Read More]