<p>See also Yann Régis-Gianas PhD thesis work with François Pottier: <a href="http://cristal.inria.fr/~fpottier/publis/regis-gianas-pottier-hoarefp.pdf">A Hoare Logic for Call-by-Value Functional Programs (MPC'08)</a>. This work was extended to cover the usual ML side-effects by Johannes Kanig and Jean-Cristophe Filliatre in 2009: <a href="http://hal.inria.fr/hal-00777585">Who: A Verifier for Effectful Higher-order Programs</a>.</p>

CC BY-SA 3.0
2014-09-19T15:13:43.637Z
2014-09-19T15:13:43.637Z
gasche
<p>You might want to check out <a href="http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/">Liquid Haskell</a>, which allow working with type <em>refinements</em> 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 <a href="http://research.microsoft.com/en-us/projects/fstar/">$F^*$ language</a>, which offers similar constructs.</p>

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

<p>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.</p>

CC BY-SA 3.0
2014-10-10T06:36:40.637Z
*without too much trouble* - not really. Idris is strict by default, and Haskell is lazy; that alone poses as a major problem. Compatibility with Haskell was also never a very high priority for Idris design.
Bartek Banachewicz
CC BY-SA 3.0
2014-10-10T15:02:29.847Z
Fair enough. Agda checks termination by default though, so things like strictness aren't a problem *in theory*. Of course run-time could be dramatically different.
cody
CC BY-SA 3.0
2014-09-19T14:42:33.973Z
2014-09-19T14:42:33.973Z
cody
<p>There is a paper in this year's <a href="http://icfpconference.org/icfp2014/">ICFP</a>, <a href="http://dl.acm.org/authorize.cfm?key=N87776">refinement types for Haskell</a>. The paper deals with termination checking rather than full Hoare logic, but hopefully that's a start in this direction.</p>

<p>The related work section in that paper contains some pointers, such as Xu, Peyton-Jones, and Claessen's <a href="http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/HaskellContract.ps">static contract checking for Haskell</a>, and Sonnex, Drossopoulou, and Eisenbach's <a href="http://pubs.doc.ic.ac.uk/zenoTwo/zenoTwo.pdf">Zeno</a> and Vytiniotis, Peyton-Jones, Claessen, and Rosen's <a href="http://research.microsoft.com/en-us/um/people/simonpj/Papers/verify/hcc-popl.pdf">Halo</a>.</p>

CC BY-SA 3.0
2014-09-19T14:33:58.880Z
2014-09-19T14:39:25.360Z
2014-09-19T14:39:25.360Z
Ohad Kammar
<p>Our work on soft verification of contracts is related, at <a href="http://dl.acm.org/citation.cfm?id=2384655" rel="nofollow">OOPSLA 2012</a> and <a href="http://dl.acm.org/citation.cfm?id=2628156" rel="nofollow">ICFP 2014</a>, 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.</p>

CC BY-SA 3.0
2014-10-10T04:29:18.917Z
2014-10-10T04:29:18.917Z
Sam Tobin-Hochstadt
<p>Honda and Yoshida's </p>

<ul>
<li><a href="http://www.doc.ic.ac.uk/~yoshida/paper/polyrec.ps">A Compositional Program Logic for Polymorphic Higher-Order Functions</a> </li>
</ul>

<p>(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:</p>

<ul>
<li><a href="http://www.doc.ic.ac.uk/~yoshida/paper/icfp04.ps">From Process Logic to Program Logic</a></li>
</ul>

<p>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:</p>

<ul>
<li><p><a href="http://www.sussex.ac.uk/Users/mfb21/publications/icfp05/index.html">An Observationally Complete Program Logic for Imperative Higher-Order
Functions</a></p></li>
<li><p><a href="http://www.doc.ic.ac.uk/~yoshida/paper/alias_jfp.pdf">A Logical Analysis of Aliasing in Imperative Higher-Order Functions</a> </p></li>
<li><p><a href="http://arxiv.org/pdf/0806.2448.pdf">Logical Reasoning For Higher-Order Functions With Local State</a> </p></li>
<li><p><a href="http://www.sussex.ac.uk/Users/mfb21/publications/fsen09">Program Logics for Sequential Higher-Order Control</a></p></li>
<li><p><a href="http://www.sussex.ac.uk/Users/mfb21/publications/lpar10">Program Logics for Homogeneous Meta-Programming</a></p></li>
</ul>

<p>The logics mentioned are what is called observationally complete, meaning that the operational and the logical semantics coincide. <a href="http://www.chargueraud.org/">Arthur Charguéraud</a> used this completenss
for his work on verifying functional programs Hoare-style in Coq.</p>

CC BY-SA 3.0
2014-09-19T17:46:25.923Z
2014-09-19T17:46:25.923Z
Martin Berger
<p><a href="http://frama-c.com/acsl.html" rel="nofollow">ACSL</a> (Ansi C Specification Language), is a specification for C code, annotated with special comments, that allows C code to be formally verified.</p>

<p>I have not looked into it, but I imagine that the formal methods used in <a href="http://frama-c.com/acsl.html" rel="nofollow">ACSL</a> 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.</p>

<p>Has anyone made something similar to <a href="http://frama-c.com/acsl.html" rel="nofollow">ACSL</a>, but for a pure functional language? If not, has there been any research into specification-annotated style formal verification for functional languages? </p>

<p>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.</p>

<lo.logic><pl.programming-languages><functional-programming><formal-methods><haskell>
Are there any annotated formal verification systems for pure functional programming languages?
Nathan BeDell
# Are there any annotated formal verification systems for pure functional programming languages?

(Asked by: username_0 on 2014-09-19)

[ACSL](http://frama-c.com/acsl.html) (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](http://frama-c.com/acsl.html) 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](http://frama-c.com/acsl.html), 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.

**Tags:** lo.logic, pl.programming-languages, functional-programming, formal-methods, haskell


---

## 5 answers

### Answer by username_6 on 2014-09-19. Score: 13 | Accepted answer

Honda and Yoshida's

* [A Compositional Program Logic for Polymorphic Higher-Order Functions](http://www.doc.ic.ac.uk/~yoshida/paper/polyrec.ps)

(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](http://www.doc.ic.ac.uk/~yoshida/paper/icfp04.ps)

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](http://www.sussex.ac.uk/Users/mfb21/publications/icfp05/index.html)
* [A Logical Analysis of Aliasing in Imperative Higher-Order Functions](http://www.doc.ic.ac.uk/~yoshida/paper/alias_jfp.pdf)
* [Logical Reasoning For Higher-Order Functions With Local State](http://arxiv.org/pdf/0806.2448.pdf)
* [Program Logics for Sequential Higher-Order Control](http://www.sussex.ac.uk/Users/mfb21/publications/fsen09)
* [Program Logics for Homogeneous Meta-Programming](http://www.sussex.ac.uk/Users/mfb21/publications/lpar10)

The logics mentioned are what is called observationally complete, meaning that the operational and the logical semantics coincide. [Arthur Charguéraud](http://www.chargueraud.org/) used this completenss
for his work on verifying functional programs Hoare-style in Coq.


---

### Answer by username_2 on 2014-09-19. Score: 15

You might want to check out [Liquid Haskell](http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/), 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](http://research.microsoft.com/en-us/projects/fstar/), 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.

> **Comments:**
> **username_3**: *without too much trouble* - not really. Idris is strict by default, and Haskell is lazy; that alone poses as a major problem. Compatibility with Haskell was also never a very high priority for Idris design.  
> **username_2**: Fair enough. Agda checks termination by default though, so things like strictness aren't a problem *in theory*. Of course run-time could be dramatically different.  

---

### Answer by username_1 on 2014-09-19. Score: 11

See also Yann Régis-Gianas PhD thesis work with François Pottier: [A Hoare Logic for Call-by-Value Functional Programs (MPC'08)](http://cristal.inria.fr/~fpottier/publis/regis-gianas-pottier-hoarefp.pdf). 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](http://hal.inria.fr/hal-00777585).


---

### Answer by username_4 on 2014-09-19. Score: 8

There is a paper in this year's [ICFP](http://icfpconference.org/icfp2014/), [refinement types for Haskell](http://dl.acm.org/authorize.cfm?key=N87776). 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](http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/HaskellContract.ps), and Sonnex, Drossopoulou, and Eisenbach's [Zeno](http://pubs.doc.ic.ac.uk/zenoTwo/zenoTwo.pdf) and Vytiniotis, Peyton-Jones, Claessen, and Rosen's [Halo](http://research.microsoft.com/en-us/um/people/simonpj/Papers/verify/hcc-popl.pdf).


---

### Answer by username_5 on 2014-10-10. Score: 1

Our work on soft verification of contracts is related, at [OOPSLA 2012](http://dl.acm.org/citation.cfm?id=2384655) and [ICFP 2014](http://dl.acm.org/citation.cfm?id=2628156), 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.


---

