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

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

(meta) edit request...

Could someone please edit this post? The block quotes contain several unusual characters that are breaking the RSS feed...

Done, I tried to remove unusu

Done, I tried to remove unusual characters, please let me know if any of these still there ...

Shortly discussed

here as well.

I am still interested in other people's experiences on this topic, by the way.

In a paper about SPeeDI the authors report sufficient performance for their Haskell implementation, but they are rather short on details.

Java

However, it turned out in our discussions that none of us were enthusiastic about the idea of using a functional language for a future verification tool, because of their impoverished environments compared with mainstream programming languages.

I'd like to hear more about the superior features in mainstream development environments.

development environment != IDE

... just to clear up possible misunderstandings.

Section 5 of the paper gives details about Haskell's and SML's language environments: available compilers, libraries, tools, documentation, performance, etc.

A few things (documentation) improved in the mean time, but not all.

Ditto

I would like to hear on your current opinion.

Oh yeah, these partly agree with you: John Launchbury, Jeff Lewis and Byron Cook On embedding a microarchitectural design language within Haskell

[And I guess I should comment that I absolutely love Haskell. It's fine, it rocks, it just has some problems like any other language]

Pretty much the same

...opinion as in the paper. Some things improved notably (documentation), others did not (yet) or not significantly. But I will keep watching. ;-)

[And I guess I should comment that I absolutely love Haskell. It's fine, it rocks, it just has some problems like any other language]

Absolutely. I am using Haskell and Common Lisp for all my prototyping needs, and both work really well there in my opinion.