Video details

Neighborhoods Banding Together: Reasoning Globally about Programs - Lisa Lippincott - CppCon 2020

English --- Our most detailed reasoning about programs is done locally: we consider a neighborhood of a program — usually a single function and the interfaces surrounding it — and reason about its behavior without reference to the remainder of the program. But this reasoning is in service of a larger goal: we want to ensure that the entire program behaves correctly.
In this talk, I will take local reasoning for granted, and look at the process of joining neighborhoods of local reasoning together, and the global reasoning that ensures they form a coherent whole. I will show how we can prevent incoherent joining, and prevent the emergence of unbounded non-local recursion as the program is linked together.
This talk builds upon the discussion of local reasoning in last year's talk "The Truth of a Procedure,” but is intended to be understandable independently.
--- Lisa Lippincott designed the software architectures of Tanium and BigFix, two systems for managing large fleets of computers. She's also a language nerd, and has contributed to arcane parts of the C++ standard. In her spare time, she studies mathematical logic, and wants to make computer-checked proofs of correctness a routine part of programming.
--- Streamed & Edited by Digital Medium Ltd - [email protected]