Weekly News - #19

Discord’s default experiment metrics had ballooned to roughly fifty, which meant Benjamini-Hochberg corrections for multiple comparisons were suppressing genuine effects and making real changes harder to detect. By collapsing correlated metrics using PCA and reducing the default set to about fifteen distinct concepts, the team improved its ability to catch moderate real effects by roughly forty-five percent.

1Password applied agentic tooling to analyze and decompose a multi-million-line Go monolith, finding that agents excel at deterministic, bounded tasks like generating call-site manifests but struggle with irreversible sequencing decisions such as schema backfills and deployment ordering. The real bottleneck in agentic refactoring is not code generation but defining explicit invariants and escalation paths, because agents will speculate with locally reasonable assumptions that are globally wrong when specifications are incomplete.

Lean's dominance in the conversation around mathematical formalisation obscures nearly sixty years of success by AUTOMATH, ACL2, HOL Light, and Isabelle, which all proved deep theorems without dependent types. Isabelle pairs the most powerful automation available with a proof syntax designed for human reading, which means it is the strongest alternative for anyone not already embedded in Lean's ecosystem.

RF engineering is rebounding sharply after two decades of decline because commercial space constellations, 5G densification, automotive radar mandates, and IoT growth are all demanding hardware-level wireless expertise at the same time. While the need has multiplied, the supply of engineers has not, which means the talent shortage is structural and companies are now building university partnerships and paying six-figure premiums rather than waiting for the academic pipeline to recover.