CppCon 2020

If the all_of() track is full, then join us in generate_n() as the overflow room.


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.