Re: [tlaplus] Re: Is TLA+ still useful if your implementation language is a purely functional one, like Haskell?

[Peter Hancock <postm...@xxxxxxxxxxxxxx>]

Ron,

Thanks for your comments, that deserve a more detailed response than I can give right now.

I'd like to understand better "where you are coming from". Broadly speaking, it seems
that faced with a specification, about the part of the universe that one wants to get
to behave in a certain way (say, the contents of a terminal open on my display, or where
a piece of artillery points in the sky), it doesn't a priori matter whether one decides
that a computer should be involved, let alone what kind of programming language one
should write the code in to load into that computer.  Do('nt) you  agree?  It might
be a bunch of people in a room with slide rules, passing around numbers written on post-its,
finally telling the gunners where to point their weapon.

There seems to be something highly distracting about functional programming, that
reminds me of those occasions when I look all over the house for my glasses and
then find them on my nose.  If we spend a lot of time in a REPL loop, as in ghci,
we get so fascinated by the "E" that we forget about the "R" and the "P".

I'd like to think that "programming" is essentially a matter of figuring out how
to bring about desired behaviours, and avoid bringing about undesired ones. 
In real life though, as we all know, "programming" is often a matter of 
clarifying and understanding a specification, and ruefully asking ourselves whether
it really captures anything intelligible a sensible person might intend. 
It seems to me one of the great benefits of decades of work on specification,
TLA+, predicate transformers or whatever, is that it rubs our noses 
in this "sharp end" of programming.

There's a lot to be said about how one figures out a candidate implementation of 
a specification using a functional programming language, how type systems might help
or hinder.  Personally, this stuff fascinates me, and I'd be delighted to discuss it with
you (though it probably shouldn't be in this forum!). 

My remarks above seem to me rather anodyne and unexceptional, no doubt
could be better expressed, and I may have entirely missed your point(s?). 
Have I said something you take exception to?  

With respect,
Peter Hancock