We’ve started a podcast! @awsto.bsky.social and @samps.phd host “Current Continuation,” a little interview series with PL researchers. The first two episodes are with @ranjitjhala.bsky.social and @satnam6502.bsky.social. sigplan.org/cc/
The work winning this year's Nobel Prize in Chemistry is science-fiction-like-materials-wizardry, but this insight about people from one of the winners (also a UCB alumnus!) is particularly profound: www.nytimes.com/2025/10/08/s...
In this episode of Current Continuation, Adrian Sampson and I talk to Prof. Sarah E. Chasins of UC Berkeley. Sarah does awesome work at the intersection of PL, HCI, and social science! Enjoy!
www.youtube.com/watch?v=9NPI...
🚀 Announcing QECLean, our effort to formalize quantum error correction and fault-tolerance in Lean. The effort is led by PhD student, Stavan Jain.
We have a full formalization of the Toric Code and a proof of its distance, [[2L^2, 2, L]]! And more to come...
Times are changing: Today, having a mechanized formal foundation enables AI agents to automatically discover and check new codes. QECLean is the foundation for AI agents to autonomously new error-correction schemes and push the frontiers of quantum computing.
LSU is using this in their quantum computing course: arxiv.org/pdf/2511.02844
"Students begin with ... QWLA, a lightweight simulation framework that supports intuitive engagement with core quantum ideas without requiring prior knowledge of matrix algebra."
