Are there any annotated formal verification systems for pure functional programming languages?

Question

ACSL (Ansi C Specification Language), is a specification for C code, annotated with special comments, that allows C code to be formally verified.

I have not looked into it, but I imagine that the formal methods used in ACSL verifiers would be similar to Hoare Logic. For pure functional languages though, such as Haskell, I can't imagine what sort of formalism would be used for formal verification.

Has anyone made something similar to ACSL, but for a pure functional language? If not, has there been any research into specification-annotated style formal verification for functional languages?

I know that there's dependent typing, which many languages (Agda, Idris, etc...) support, but in Haskell dependent typing is difficult without doing some (unreadable?) type-wizardry. With that in mind, and since Haskell has so much better library support than Agda and Idris, I believe such a system for functional formal verification might be useful, but I don't know if research has been done on this or not.

Answer 1

Honda and Yoshida's

• A Compositional Program Logic for Polymorphic Higher-Order Functions

(probably) pioneered Hoare logics for purely functional languages. This work is based on Hennessy-Milner logic and Milner's encoding of functions into processes, as described here:

• From Process Logic to Program Logic

The work by Régis-Gianas et al mentioned in another answer is similar to the first work above by Honda/Yoshida. This has been extended to effectful ML-style languages:

• An Observationally Complete Program Logic for Imperative Higher-Order Functions

• A Logical Analysis of Aliasing in Imperative Higher-Order Functions

• Logical Reasoning For Higher-Order Functions With Local State

• Program Logics for Sequential Higher-Order Control

• Program Logics for Homogeneous Meta-Programming

The logics mentioned are what is called observationally complete, meaning that the operational and the logical semantics coincide. Arthur Charguéraud used this completenss for his work on verifying functional programs Hoare-style in Coq.

Answer 2

You might want to check out Liquid Haskell, which allow working with type refinements rather than dependent types. Type refinements can be seen as a restricted logical language that allow you to express Hoare-style properties of the inhabitants of various datatypes. Another possible candidate is the $F^*$ language, which offers similar constructs.

There seems to be a close correspondence between refinement types and the ACSL like notations.

Finally I can only suggest taking a closer look at Agda and Idris, as they can compile to Haskell, and are aimed at providing the user with a usable programing language (especially Idris). I suspect it's possible to integrate Haskell libraries into Idris code without too much trouble.

Answer 3

See also Yann Régis-Gianas PhD thesis work with François Pottier: A Hoare Logic for Call-by-Value Functional Programs (MPC'08). This work was extended to cover the usual ML side-effects by Johannes Kanig and Jean-Cristophe Filliatre in 2009: Who: A Verifier for Effectful Higher-order Programs.

Answer 4

There is a paper in this year's ICFP, refinement types for Haskell. The paper deals with termination checking rather than full Hoare logic, but hopefully that's a start in this direction.

The related work section in that paper contains some pointers, such as Xu, Peyton-Jones, and Claessen's static contract checking for Haskell, and Sonnex, Drossopoulou, and Eisenbach's Zeno and Vytiniotis, Peyton-Jones, Claessen, and Rosen's Halo.

Answer 5

Our work on soft verification of contracts is related, at OOPSLA 2012 and ICFP 2014, allows you to write contracts, which are a lot like ACSL specs, and then either statically verify them or use them a dynamic checks at runtime.