[Haskell-cafe] formal methods & functional programming

[Robin Green]

Abigail wrote:
> Hi,
> I have been searching papers about tha raltionship
> between formal methods in software engineering and
> functinal programmming, but i haven't found enough
> information.

Functional programming in pure functional languages like Haskell can 
help to make programs easier to reason about - but it doesn't _remove_ 
the need for formal methods.

For example, there are laws about certain classes such as Monad and 
Monoid which all instances of those classes must follow in order to be 
considered "proper" Monads or Monoids. However, in order to reason about 
functions defined over all Monads (say), we need to know that those laws 
hold for _all_ possible Monads (without laws, we don't really know 
anything about the methods of Monad - in a non-strict language, the 
methods might not even be well-defined for certain inputs). But Haskell 
doesn't even have a way to _state_ these laws formally, much less 
_prove_ them!

I am working on a functional programming and specification language in 
my spare time which does have such formal methods features built-in, but 
it is not even implemented yet. (I can email you if I ever write a paper 
on it, but it may be some years before that happens.)

However, there are various other angles which you can research:

1. Proofs as programs: _Constructive_ proofs of theorems can be 
automatically converted into programs in a functional programming 
language - although these programs are not always efficient. Indeed it 
is possible that a generated program will be far too inefficient to be 
useful. See for example "Proofs, Programs and Executable Specifications 
in Higher Order Logic", a Phd thesis by S Berghofer at 
http://www4.in.tum.de/~berghofe/papers/phd.pdf

1a. Models as functional programs: The very first sentence in Chapter 1 
of the thesis I just cited, says: "Interactive theorem provers are tools 
which allow [one] to build abstract system models, often in some kind of 
functional programming language involving datatypes and recursive 
functions."

2. Dependent types: By programming in a dependently-typed functional 
programming language such as the research language Epigram, it is 
possible to write functional programs whose types force them to be 
correct. See for example "Why Dependent Types Matter" by Thorsten 
Altenkirch, Conor McBride, and James McKinna. However, in my opinion 
this is only useful for simple "sized types" such as "a list of length 
6". For more complicated properties, I believe this approach is 
unnecessarily difficult, and does not match how mathematicians or 
programmers actually work. My approach (see above) clearly separates the 
programming, the theorems and the proofs, and (in principle) allows all 
three to be written in a fairly "natural" style. As opposed to dependent 
types which, in Epigram at least, seem to require threading proofs 
through programs (for some non-trivial proofs).

3. Separate formal methods tools for Haskell: My approach is to 
integrate formal methods directly into the essential core of a language, 
but this is quite unusual to say the least - a more normal thing to do 
(whether for functional or imperative languages) is prepare a separate 
formal methods tool for an existing programming language. This has been 
done for Haskell - see "Verifying haskell programs using constructive 
type theory" by Abel et. al. at 
http://portal.acm.org/citation.cfm?id=1088348.1088355

I have not considered testing in this email because another email 
already mentioned QuickCheck.
-- 
Robin