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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Fri, 16 Oct 2015 03:50:59 -0700 (PDT)*Cc*: zans....@xxxxxxxxxxxxxx*References*: <a97c6b33-de29-473f-9515-42b70064a28c@googlegroups.com> <44d35dc7-4b80-4bbe-81f9-548b310987d6@googlegroups.com> <c114771f-f15e-4373-9501-f706bf38dbd7@googlegroups.com> <53a88485-bf93-4b8b-88cf-ed32eb78d5a7@googlegroups.com>

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

**Follow-Ups**:

**References**:**What do you think about the use of category theory for specifications?***From:*zans . . . .

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

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

**Re: What do you think about the use of category theory for specifications?***From:*zans . . . .

- Prev by Date:
**Re: What do you think about the use of category theory for specifications?** - Next by Date:
**Re: What do you think about the use of category theory for specifications?** - Previous by thread:
**Re: What do you think about the use of category theory for specifications?** - Next by thread:
**Re: What do you think about the use of category theory for specifications?** - Index(es):