proof/examples of productivety increase ?

[chris glur]

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.

[Nigel Galloway-2]

Should a language like Joy be compared to Java. Java compiles into class files, which consist of bytecodes, which is  assembler like code for the JVM.
 
Joy comes in 2 parts an iterpreter and a language. The language is more like the JVM facing Java bytecode assembler than the programmer facing Java language.
 
Java is interesting in this respect: its class files are compiled in such a way that closure is regularly achieved at the bytecode level by adding extra instructions. This means that the correctness and resource usage can be verified when the class is loaded. For efficiency the JVM reads and 'understands' the bytecodes. It does not execute them slavishly as real assmbler is by a real CPU but intelligently optimizing the instructions.

To be efficient at a programming level, a language designed for the type of problem is required. This should be compiled into Joy. The questions then are:
 
  can this Joyclass be optimized using concatative algorithms into something better than the Java class or the Intel assembler?
 
  can this be done by machine, or would it require rooms full of people hand optimizing assembler like Joy?
 
--- On Sun, 12/4/09, chris glur <crglur@...> wrote:

From: chris glur <crglur@...>
Subject: [stack] proof/examples of productivety increase ?
To: concatenative@...
Date: Sunday, 12 April, 2009, 4:42 PM








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.
















     

[Non-text portions of this message have been removed]

[William Tanksley, Jr]

Nigel Galloway wrote:
> Should a language like Joy be compared to Java.

Yes and no. A language like Joy yes; Joy itself NO. Joy is an academic
prototype, not really intended for any specific use.

> For efficiency the JVM reads and 'understands' the bytecodes. It does
> not execute them slavishly as real assmbler is by a real CPU but
> intelligently optimizing the instructions.

Right.

The concatenative language "Cat" was originally designed for this
general type of use, as an intermediate language. You might want to read
up on it. It also has a fairly advanced type checker.

-Wm