Formal Verification of Functional Programs

Question

So I've been interested in learning more about formal verification, and I've seen a lot of interesting things like ACSL and JML which are based on the concept of Hoare triples.

My question is, that these seem to be a way to describe the behaviour of imperative programs via specification languages that are mostly functional (plus universal and existential quantifiers). But I don't even know the keywords to search to start learning how one would perform formal verification of code in a pure functional language like Haskell.

Could anyone provide a link to material or the name of the equivalent/analogue of Hoare triples for pure functional computation? Or do you need a fundamentally different approach in the purely-functional realm?

Answer 1

There is probably a lot that can be said about this subject.

I'll just mention one broad approach: types. Sufficiently expressive type systems allow you to express interesting constraints on your programs. This isn't unique to pure functional programming, but such languages have a reputation of taking it farther than statically typed imperative languages. Haskell already has an expressive type system, and compiler-specific extensions allow you to write even more expressive types.

Ideally, you would be able to write a function and its type signature and if the code compiled, then you would have verified that the implementation of your function corresponds to your specification, namely your type signature. It's not quite that simple in Haskell, though, since its type system is unsound:

x :: a -> b
x = x

The above code will compile, even though that might seem a bit objectionable.

The problem is that Haskell allows such functions to potentially be non-terminating, or to effectively crash. In turn, it lets all types be inhabited by bottom, the computation that never completes successfully.

But, if we crank up the types to 8, we are able to transcend such inconsistencies by imposing some limitations on what our programs can express. Namely, if we are willing to force certain types of functions to be terminating, and to only use such terminating functions as building blocks in other terminating functions, we have gained some of our ability to reason about types back. This is called total functional programming, and now we might with more confidence equate our types with being theorems, and our programs with being proofs of such theorems.

Now we just need to crank up our types to 11 in order to reach the heights of the most expressive types that seem to have been implemented in programming languages to this day, namely dependent types. Such type systems lets you express arbitrary properties about your programs. The backside to such power is responsibility - you might have to take care to prove that your code actually implements whatever your types states that it should.

---

I think that types are very natural path to take for people who are both interested in static functional programming languages and some level of formal verification. Static functional programming languages, like Haskell, already try to encourage a certain rigour with regards to how one structures one's programs such as to take maximum benefit from the capabilities of the type system. Exploring the power and expressibility that types can bring - either as type system extensions in Haskell, or as in full-on proof assistants - can be a very natural extension of that.

Answer 2

You also use Hoare triples. See e.g.

• Honda, Yoshida, A Compositional Program Logic for Polymorphic Higher-Order Functions.
• Berger, Program Logics for Sequential Higher-Order Control.
• Berger, Tratt, Program Logics for Homogeneous Meta-Programming.

You need triples even for pure functional languages because they too have an effect, namely termination. The precondition establishes whether the program exhibits this effect or not. The post-condition describes the output value.