[stack] proof/examples of productivety increase ?

On cleaning out archives of
Tue, Apr 29, 2008 at 10:20 AM
where John Nowak wrote:

>Most type systems are not compositional which destroys the simple
>algebra of concatenative programs. Take these equivalencies
>for example:

>  [$A] i == $A -- application
>  [$A] [$B] o == [$A $B] -- composition
>  $a [$B] pa == [$a $B] -- partial application
>  [$A] m == [$A] $A -- self-application

>Unfortunately, all of these rules (except perhaps for partial
>application) fall apart once types are involved. This is of
>practical concern as it makes cut-and-paste refactoring
>impossible and will cause problems with many macro
>transformations.

I wondered is there a tutorial on 'algebra of concatenative
programs', preferably without another new syntax,
which shows complete examples of design and/or correctness proof ?

Some time back I did a string-utility.  Something like:
remove all non-line-leading repeated spaces in all lines,
and was amazed at the complexity, with the nested loops and several
pointers needed.  And I recently gave back a book which told about
the well-know Hi-priest who published about 'correctness proofs'
and later 2 guys found 2 errors and yet later someone else found
another error. Does anyone know of a link to this story ?
I think it was in the '70s ..Parnas...Hoare..days.

Frankly, this concat-business seems pointless to me unless it can
increase productivety, which IMO is only possible by:
1. being more readable - eg. by being closer to the mental model
  of the problem/S. Which I don't think it is eg. compared to
  typical java or Algol-family code ..... Eiffel ?...;
2. being ameniable to formal correctness proof techniques, eg.
  via transformations, by its algebra.

The newsgroup/s re. 'formal methods' only have lists of conferences.
Like snake-oil-peddlars: pay for an attendance and get a key to
the inner secrets.   For decades formal methods have been the
'real soon now magic bullet'.  Like epaper seems to be lately.

I want some concrete demonstrations.
Starting from 'hello world' level and extending to usefull
utilities. BTW who can demonstrate cat's benefit on a string
utility, like above or similar ?

Thanks,

== Chris Glur.