10
$\begingroup$

I want to provide proofs for parts of a Haskell program I'm writing as part of my thesis. So far however, I failed to find a good reference work.

Graham Hutton's introductory book Programming in Haskell (Google Books)—which I read while learning Haskell—touches on a few techniques for reasoning about programs such as

  • equational reasoning
  • using non-overlapping patterns
  • list induction

in chapter 13 but it's not very in-depth.

Are there any books or article you can recommend which provide a more detailed overview of formal proving techniques for Haskell, or other functional, code?

$\endgroup$
5
$\begingroup$

One of the de facto methods for proving results in functional programming is via Richard Bird's group.

In particular, you ask for an in-depth or at least more comprehensive approach to equational reasoning and list induction and this is provided in Lectures on Constructive Functional Programming.

More generally, the text "Algebra of Programming", by Bird and de Moor, also deals with the correctness of functional algorithms such as optimisation and dynamic programming problems.


If you come across other useful resources for this problem, please mention them and perhaps we can turn this post into a wiki.

$\endgroup$
  • $\begingroup$ Thank you! Sure, if I find more ressources, I will make sure to add them to my post. $\endgroup$ – FK82 Sep 12 '16 at 16:27
6
$\begingroup$

You can start with

Topics include basic concepts of logic, computer-assisted theorem proving, the Coq proof assistant, functional programming, operational semantics, Hoare logic, and static type systems. The exposition is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers. No specific background in logic or programming languages is assumed, though a degree of mathematical maturity will be helpful.

You can skip (or skim) the programming language theory parts and only learn how to deal with formal proofs starting from Preface up to IndPrinciples. The book is really well-written and illuminating.

Then you might want to proceed with

In this volume you will learn how to specify and verify (prove the correctness of) sorting algorithms, binary search trees, balanced binary search trees, and priority queues. Before using this book, you should have some understanding of these algorithms and data structures, available in any standard undergraduate algorithms textbook. You should understand all the material in Software Foundations Volume 1 (Logic Foundations)

A note of warning: VFA is still in beta-release!

$\endgroup$
  • $\begingroup$ (Your second link directs to the wrong place.) Also, there is Verified Functional Programming in Agda; which uses Agda, formally a programming language but uses unicode and so is closer to math notation. $\endgroup$ – Musa Al-hassy Sep 14 '16 at 14:57
  • $\begingroup$ Corrected, thanks. Yes, I've read VFPiA, but it is not to my taste. $\endgroup$ – Anton Trunov Sep 14 '16 at 17:11
  • $\begingroup$ Thank you for your answer! I think there is a misconception. I'm not looking for functional techniques for proving algorithms (such as a proof assistant), but for techniques for proving functional code (for example for proving a functional implementation of a given algorithm correct) @MusaAl-hassy answer is very close to my desired answer. In case I missed it and the books you cited cover this aspect as well, would you mind adding the relevant chapters? $\endgroup$ – FK82 Sep 17 '16 at 14:22
  • $\begingroup$ @FK82 Here is a Theorem app_assoc : ∀ l1 l2 l3 : natlist, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3) from the Lists chapter. Does this example look anything like the thing you're interested in? They start with functional programming in Coq, but then move on to reasoning about the properties of functional programs. The chapters from Preface up to IndPrinciples cover both of those, and I'd say programming and reasoning are intertwined there. $\endgroup$ – Anton Trunov Sep 17 '16 at 15:34
  • 1
    $\begingroup$ @FK82 (1) I totally agree with this comment. (2) You might want to look at the book "Thinking Functionally with Haskell" (2015) by R. Bird. The book has tons of examples of reasoning about Haskell. (3) Also, "Pearls of Functional Algorithm Design" (2010) by the same author may be of some help to you. $\endgroup$ – Anton Trunov Sep 18 '16 at 15:38
5
$\begingroup$

It turns out that an excellent source of proof techniques and examples for proving things about pure functional languages is proof assistants which usually include as part of their specification language a pure functional language on which it is possible to reason equationally.

One might want to consult a book like Certified Programing with Dependent Types for an in-depth introduction to this kind of reasoning in a specific proof assistant, namely Coq.

$\endgroup$
  • $\begingroup$ Thanks! I'm actually looking specifically for techniques in Haskell. My post was edited to include all functional code, but that's well above my intentions. $\endgroup$ – FK82 Sep 17 '16 at 14:25
  • 1
    $\begingroup$ I'm not aware of systems designed to verify Haskell specifically, but I would note that 1) The functional core of Coq (and Agda) is essentially indistinguishable from that of Haskell (except for the restriction to total functions) and 2) Programs verified in Coq and Agda can be extracted to Haskell (though I believe extraction to Haskell is better supported in Agda, where Coq is more Ocaml-centric) $\endgroup$ – cody Sep 18 '16 at 13:13
  • $\begingroup$ Good to know! This would however imply that I rewrite my program (or the relevant parts) in Coq or Agda. I don't think that's reasonable in my case. $\endgroup$ – FK82 Sep 19 '16 at 13:40
  • $\begingroup$ There are a couple of very experimental "front ends" that try to convert Haskell to Isabelle or directly prove equivalences using Isabelle, but I wouldn't hold too much stock in their maturity. I think re-writing the code would ultimately be less work. $\endgroup$ – cody Sep 19 '16 at 15:37
4
$\begingroup$

I suggest to use program logics. They deal much better with effects than typing systems.

There are numerous program logics for functional languages. This becomes interesting with effects. See e.g. Logical Reasoning for Higher-Order Functions with Local State.

Work by Arthur Charguéraud integrates the program logic approach with proof assistants, see e.g. this overview page.

$\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.