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

*From*: George Singer <george....@xxxxxxxxx>*Date*: Wed, 11 Jan 2017 19:45:10 -0800 (PST)*References*: <2de00f5b-0cc4-4528-bc27-e24a1a244ce5@googlegroups.com> <1d53a3db-83bb-4b73-a4ec-e5739095d548@googlegroups.com>

Leslie — I’m watching the video you posted. It’s great.

As you make clear, the language you’re using is

irrelevant. It’s whether you’re writing a simple functional program

or a reactive program—that is, implementing a system.

Why is a (purely) functional program not considered a system? Does “system” imply state transitioning?

One other possible use of TLA+ for functional programs that you didn’t

mention is in coming up with an algorithm to compute the function.

The complexity of an algorithm is how many steps it takes to execute.

The complexity of a function is the smallest number of steps it takes

to compute it. That’s not a practically useful concept of complexity.

The complexity of sorting is N log N, but if I write bubble sort in a

functional language, the complexity of the function I’ve defined is

N log N, but no compiler is going to produce a program with that

complexity. I expect that there are many algorithms that are easier

to think of imperatively than functionally. It may be because

I’m used to programming imperatively.

I’m assuming here your point is that (as it relates to TLA+), in a purely functional language, one can wrap a pure function interface over an imperative algorithm and, when doing so, use TLA+ to help specify various safety and liveness properties of the algorithm.

On Wednesday, January 11, 2017 at 5:43:48 PM UTC-5, Leslie Lamport wrote:

I find your argument sound, though the subject of the posting is

misleading. As you make clear, the language you're using is

irrelevant. It's whether you're writing a simple functional program

or a reactive program--that is, implementing a system.

You should mention that the TLA+ tools were not optimized for

evaluating functions. While writing a mathematical specification of a

functional program may help you understand what you're doing, the

tools might not be useful in helping you to debug it. If the tools

can't find errors in your spec, you might be better off writing an

informal spec rather than a formal TLA+ spec.

A benefit of using TLA+ is that it teaches you to think

mathematically, which teaches you to write better informal specs. In

particular, it teaches you to think above the code level--meaning at a

level at which the language you're using is irrelevant. An example

is the TLA+ pretty-printer in my lecture "Programming Should be More

than Coding", which is at

https://www.youtube.com/watch?v=6QsTfL-uXd8

One other possible use of TLA+ for functional programs that you didn't

mention is in coming up with an algorithm to compute the function.

The complexity of an algorithm is how many steps it takes to execute.

The complexity of a function is the smallest number of steps it takes

to compute it. That's not a practically useful concept of complexity.

The complexity of sorting is N log N, but if I write bubble sort in a

functional language, the complexity of the function I've defined is

N log N, but no compiler is going to produce a program with that

complexity. I expect that there are many algorithms that are easier

to think of imperatively than functionally. It may be because

I'm used to programming imperatively.

Leslie

**References**:

- Prev by Date:
**Re: Is TLA+ still useful if your implementation language is a purely functional one, like Haskell?** - Next by Date:
**Re: Is TLA+ still useful if your implementation language is a purely functional one, like Haskell?** - Previous by thread:
**Re: Is TLA+ still useful if your implementation language is a purely functional one, like Haskell?** - Next by thread:
**Re: Is TLA+ still useful if your implementation language is a purely functional one, like Haskell?** - Index(es):