6
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ It's worth noting that dependently typed programs are a somewhat different approach since they are correct by construction. That is, with Hoare triples you write your program, then check if you can prove that it's correct. With dependent types, you write a correctness proof as part of your program. $\endgroup$ – jmite Mar 5 '15 at 9:07
  • 1
    $\begingroup$ @jmite I should have made clear that I tried to answr the broad "formal verification of functional programs", not the part about Hoare triples in particular. :) But maybe that was a bit off-topic; maybe the OP only wanted to know about Hoare triples in FP, or something else if that didn't exist. $\endgroup$ – Guildenstern Mar 5 '15 at 12:47
2
$\begingroup$

You also use Hoare triples. See e.g.

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.