Hillel Wayne posted a challenge to find out whether functional programs are really easier to verify than imperative ones, as some claim. There were three problems, and I am posting Coq solutions here (two of them by myself).

Padding

The first challenge was to prove the correctness of a padding function. Given a padding character c, a length n and a sequence s, left_pad c n s should pad s with c on the left until its size reaches n. If the original string is larger than n, the function should do nothing. My implementation is similar to other solutions on the web, and reuses functions and lemmas available in the Math Comp libraries.

The call to nseq creates a constant sequence with the number of cs that needs to be added, and appends that sequence to s. Note that subtraction is truncated: n - size s is equal to 0 when n <= size s. As the specification for left_pad, I am taking the properties that were verified in the original solution in Hillel's post, which was written in Dafny. My proofs are not automated like in Dafny, but still fairly easy. (The statements are slightly different because they use the nth function to index into a sequence, which requires a default element to return when the index overflows.)

Interestingly, these properties completely characterize the result of left_pad: any function f that satisfies the same specification must produce the same output.

Some fans of functional programming claim that it obviates the need for verification, since the code serves as its own specification. Though exaggerate (as we will see in the last problem), the claim does have a certain appeal: the definition of left_pad is shorter and more direct than the specification that we proved.

Unique

The second problem of the challenge asked to remove all duplicate elements from a sequence. I decided not to include a solution of my own here, since the Math Comp library already provides a function undup that does this. We had to show that the set of elements in its output is the same as in its input, and that no element occurs twice, properties that are both proved in Math Comp (mem_undup and undup_uniq). Hillel wrote that imperative programs had an advantage for this problem because of its symmetry. I am not sure what was meant by that, but the Dafny and the Coq proofs are comparable in terms of complexity. (To be fair, Dafny has better automation than Coq, but this has probably little to do with being functional or imperative: other functional provers fare better than Coq in this respect as well.)

Fulcrum

The last problem was also the most challenging. The goal was to compute the fulcrum of a sequence of integers s, which is defined as the index i that minimizes the quantity fv s i shown below in absolute value.

The simplest way out would be to compute fv s i for all indices i and return the index that yields the smallest value. Instead of writing this program ourselves, we can just reuse the arg min function available in Math Comp.

Unfortunately, this naive implementation runs in quadratic time, and the problem asked for a linear solution. We can do better by folding over s and computing the values of fv s i incrementally. With a left fold, we can compute the fulcrum with four auxiliary variables defined in the state type below, without the need for extra stack space. (This is a bit more efficient than the original solution, which had to store two sequences of partial sums.)

On each iteration, the fulcrum_body function updates the state st given n, the current element of the sequence. The main function, fulcrum, just needs to provide a suitable initial state and return the final value of best_i.

To verify fulcrum, we first prove a lemma about foldl. It says that we can prove that some property I holds of the final loop state by showing that it holds of the initial state x0 and that it is preserved on every iteration in other words, that I is a loop invariant. The property is parameterized by a "ghost variable" i, which counts the number of iterations performed.

We complete the proof by instantiating foldlP with the fulcrum_inv predicate below. This predicate ensures, among other things, that best_i holds the fulcrum for the first i positions of the sequence s. Hence, when the loop terminates, we know that best_i is the fulcrum for all of s.

Conclusion

So, is functional really better than imperative for verification? Though I am a fan of functional languages, I will not attempt to offer a definitive answer. It is true that simple programs such as left_pad are often as good (or better) than their specifications, but some of those would be inefficient in practice, and fast implementations such as fulcrum might be tricky to verify. As mentioned in Hillel's post, the main issue when verifying imperative code is aliasing: we must argue that every call preserves the assumptions made in other parts of the code, something that comes for free with functional programming. However, if a program only modifies local state (like the Dafny solutions did), reasoning about this kind of interference becomes much more manageable. Of course, nothing prevents us from combining the benefits of functional and imperative programming. We can implement an efficient algorithm using mutable state and verify it against a specification that mixes logic and pure functions. Indeed, that is the strategy followed by the Dafny solution, and many frameworks for verifying imperative code only allow pure functions in specifications. Moreover, it is possible to define imperative languages within Coq and use the logic to verify programs in this language; this is the essence of frameworks such as VST or Iris.