[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: What do you think about the use of category theory for specifications?




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:
 
http://stackoverflow.com/questions/3252189/functional-proofs-haskell
 
than in procedural language
 
http://research.microsoft.com/en-us/um/people/lamport/tla/VoteProof.tla
 
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