Data constantly change. Google engineers make one commit every 2 seconds on the same git repository. On average, Twitter receives approximatively 6000 tweets per second. A self-driving car typically updates 100MB of its state each second.

How do we program software systems to handle these changes? When data is made of tiny flat records like tweets, and when data processing is made of only purely local algorithms like statistical operators, stream-based programming is most of the time the right approach.

What if the data is more structured, typically like a source code repository? Can we follow a similar dataflow approach? That is not clear. We believe that incremental functional programming could provide better tools for that kind of situations.

Incremental functional programming is about implementing change-centric software systems using first-class changes. From a base input and a change to this input, an incremental program computes a change of the base output. More formally, if f is a function of type A → B and if there is a type ∆A for changes over values of type A, and a type ∆B for changes over values of type B, an incrementalization D(f) of f is such that f x ⊕ D(f) x dx = f (x ⊕ dx) where ⊕ is the application of a change to a value and D(f ) has type A → ∆A → ∆B.

In this talk, we will explain why incremental functional programming is important but error-prone. We will describe our ongoing work to develop ∆Caml and ∆Coq, two tools that assist the incremental programmer in certifying incremental functional programs.