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@yahoogroups.com
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]