archives

Today's Status of Functional Programming Languages for Verification Tools ?

An interesting conclusion based on the ML and Haskell implementations existing in October, 2002 comes from the paper "Functional Programming Languages for Verification Tools: A Comparison of ML and Haskell", by Perdita Stevens with Martin Leucker, Thomas Noll, Michael Weber
[quote]
6 Conclusion

There have been positive and negative aspects to both
our sets of experiences with Haskell and ML, as there
would doubtless have been with whatever language we
had chosen. Overall, we consider Standard ML to be a
slightly better choice for our kind of application than
Haskell, more because of a more stable environment
of supporting tools than because of language features.
Of course, there are many alternatives including other
functional languages of which we have less experience;
O'Caml might be a strong candidate. However, it turned
out in our discussions that none of us were enthusiastic
about the idea of using a functional language for a fu-
ture verification tool, because of their impoverished envi-
ronments compared with mainstream programming lan-
guages. Our conclusion is that if/when we develop new
verification tools, these will be written in \a Java-ready
subset of C++". That is, we would prefer to be writ-
ing in Java, but at present this appears premature for
performance reasons. We would write therefore in C++,
trying to avoid using features (such as multiple inheri-
tance, non-virtual functions, \friends") which cannot be
readily translated into Java.
[/quote]
What would be a conclusion of such a comparison today?

Also interesting and very true observation from the same article:

[quote]
Why is there so little material to help developers
make an informed choice? Part of the reason must be
that it is very hard to do convincing comparisons of lan-
guages without being vulnerable to the criticism that
one is not comparing like with like. We think that a fair
comparison needs to be based on real experience of peo-
ple using the languages to build real systems in the same
domain; otherwise it is almost impossible to be sure that
diferences are not due to diferences in the domains of
application. The systems themselves need to be broadly
comparable in size and complexity, need to be more than
toys, and should preferably have been developed and
maintained over years (since a language that makes de-
velopment easy might nevertheless encourage the devel-
opment of code which is unmaintainable). Moreover, the
domain should be one where either of the languages is
a reasonable choice, and the comparison should be done
by people with a reasonably typical level of experience in
the languages. A comparison is probably most generally
useful to developers when it is done neither by novices
in the languages compared nor by people intimately fa-
miliar with the compiler internals.
[/quote]
more from the same author...