Local Reasoning for Global Properties

This blog post is about a fundamental tension in software engineering: you want to write code in small, understandable chunks ("local reasoning"), but many important properties — like security, data integrity, or memory safety — depend on the whole program working correctly ("global properties"). The author, Laurie Tratt, is a professor of software development at King's College London and a designer of the Converge programming language. He argues that language features like type systems, garbage collection, and formal verification are attempts to give programmers local guarantees about global concerns. The piece draws on decades of programming language research to discuss what works (e.g., Haskell's purity) and what stretches local reasoning too far (e.g., Rust's ownership model, which forces global constraints into local decisions). Key context: "local reasoning" is a term from programming language theory popularized by John Ousterhout's "A Philosophy of Software Design" and earlier by the "modular reasoning" tradition; the post presumes familiarity with concepts like type systems, garbage collection, and borrow checking.