Do you think so? My understanding was that functional languages would be easier to specify than imperative ones as programs written in a functional style are pretty close to how mathematical functions are written.
To specify or to prove?
Specifying a function in a procedural language or a functional one amount to the same thing since
in both cases a specification is a formula expressed in a first order logic using sets, functions and relations.
Proving looks a bit different. Proofs may look simpler in a pure functional language:
than in procedural language
But I suppose that if you want to have complicated properties with quantifiers and so on,
choosing a functional language rather than a procedural one won't help.
TLAPLUS is more adapted to a procedural language so far.
(But in my post I wanted to emphasize that you also need an abundant and accurate information about
the algorithms and in that case procedural langages are better covered. Test: pick an algorithm of
your choice and try to find the documentation about all its characteristics in both a functional and a
procedural language.)
--
FL