Continuity and Robustness of Programs
Computer scientists have long believed that software is
from physical systems in one fundamental way:
while the latter have continuous dynamics, the former do
not. In this paper, we argue that notions of continuity from
mathematical analysis are relevant and interesting even
for software. First, we demonstrate that many everyday
programs are continuous (i.e., arbitrarily small changes to
their inputs only cause arbitrarily small changes to their
outputs) or Lipschitz continuous (i.e., when their inputs
change, their outputs change at most proportionally).
Second, we give an mostly-automatic framework for verifying
that a program is continuous or Lipschitz, showing
that traditional, discrete approaches to proving programs
correct can be extended to reason about these properties.
An immediate application of our analysis is in reasoning
about the robustness of programs that execute on uncertain
inputs. In the longer run, it raises hopes for a toolkit
for reasoning about programs that freely combines logical
and analytical mathematics.