chris glur — 2007-05-13 04:53:48

I've been lurking and waiting/expecting the answer to this question
to become obvious -- so far nothing.

Via a forgotten tortuous search for means which could reduce software
errors via some formal methods, perhaps transforming conventional
imperative style syntax, I came upon 'Joy'.

Q -Can concatenative languages substantially help in building
'program correctness' ? If not, what do they offer that's special ?

I'm also investigating:
http://www.rebelscience.org/Cosas/components.htm
# COSA is based on the premise that the
# primary reason that computer programs are unreliable is the
# age-old practice of using the algorithm as the basis of software
# construction. Switch to a synchronous, signal-based model
# and the problem will disappear.

Perhaps COSA too is a futile investigation ?
Thanks for any info,

== Chris Glur.

PS. I received, what I only later realised was on 'off group'
post re. Cat 0.10.4 Release now with Graphics

I've been resisting M$loth controlling IT & my life, and now gmail
[google having similarly diverted/taken-over Usenet] from where I've
registed this mail-list, has so much deliberate eye-candy distraction,
that when I see "Cat 0.10.4 Release now with Graphics", I must
assume it's from the group and not an individual.

Besides normally, cat related queries should be posted to the group ?

Christopher Diggins — 2007-05-13 17:20:15

On 5/12/07, chris glur <crglur@...> wrote:

> I've been lurking and waiting/expecting the answer to this question
> to become obvious -- so far nothing.
>
> Via a forgotten tortuous search for means which could reduce software
> errors via some formal methods,

Such as type systems?

> perhaps transforming conventional
> imperative style syntax, I came upon 'Joy'.
>
> Q -Can concatenative languages substantially help in building
> 'program correctness' ?

Not directly. They are however relatively easy to type-check.

> If not, what do they offer that's special ?

Simple semantics. Compact code. Easy to learn. Easy to implement
efficiently. Easy to analyze and manipulate algebraically.

> I'm also investigating:
> http://www.rebelscience.org/Cosas/components.htm
> # COSA is based on the premise that the
> # primary reason that computer programs are unreliable is the
> # age-old practice of using the algorithm as the basis of software
> # construction. Switch to a synchronous, signal-based model
> # and the problem will disappear.
>
> Perhaps COSA too is a futile investigation ?

This is too open-ended of a question and off-topic for this forum.

> Thanks for any info,
>
> == Chris Glur.
>
> PS. I received, what I only later realised was on 'off group'
> post re. Cat 0.10.4 Release now with Graphics
>
> I've been resisting M$loth controlling IT & my life, and now gmail
> [google having similarly diverted/taken-over Usenet] from where I've
> registed this mail-list, has so much deliberate eye-candy distraction,
> that when I see "Cat 0.10.4 Release now with Graphics", I must
> assume it's from the group and not an individual.
>
> Besides normally, cat related queries should be posted to the group ?

The discussion group at
http://groups.google.com/groups/cat-language.com is the best place for
Cat specific discussion.

Christopher Diggins
http://www.cat-language.com

William Tanksley, Jr — 2007-05-13 17:21:52

chris glur <crglur@...> wrote:

> I've been lurking and waiting/expecting the answer to this question
> to become obvious -- so far nothing.

To the best of my knowledge, the answer to that question is not
obvious to any of us. I think that if it can be answered, it will take
some real work.

> Via a forgotten tortuous search for means which could reduce software
> errors via some formal methods, perhaps transforming conventional
> imperative style syntax, I came upon 'Joy'.

Welcome in!

> Q -Can concatenative languages substantially help in building
> 'program correctness' ? If not, what do they offer that's special ?

They can because they offer (at least) one thing special: they allow
you to build small units that are correct programs, then join those
units together and know that the result is also a correct program.

This is not a magic formula, though -- "a correct program" is not
automatically "the program you meant to write". Other methods are
needed, and because the idea of a concatenative language is so new, we
don't yet know what they'll be.

> I'm also investigating:
> http://www.rebelscience.org/Cosas/components.htm
> # COSA is based on the premise that the
> # primary reason that computer programs are unreliable is the
> # age-old practice of using the algorithm as the basis of software
> # construction. Switch to a synchronous, signal-based model
> # and the problem will disappear.

> Perhaps COSA too is a futile investigation ?

I doubt it's futile; but I'm pretty sure that the description they're
giving is overblown. I don't see how you can get around the fact that
computers are extremely literal creatures, and programmers can't keep
track of everything the computer needs to be told at the same time. As
long as those things are true, I doubt that "the problem will
disappear."

Perhaps COSA will help, though. I'll read up on it; thank you for the link.

> == Chris Glur.

-Billy

Christopher Diggins — 2007-05-13 17:45:40

> > Q -Can concatenative languages substantially help in building
> > 'program correctness' ? If not, what do they offer that's special ?
>
> They can because they offer (at least) one thing special: they allow
> you to build small units that are correct programs, then join those
> units together and know that the result is also a correct program.

This is a good point, sorry I overlooked it.

As it happens this is not the case with Cat. You can't for example
concatenate non-lists or evaluate non-functions. Perhaps this means
Cat is not concatenative?!

Cheers,
Christopher

eas lab — 2007-05-14 13:54:38

Chris Glur wrote:

> > Q -Can concatenative languages substantially help in building
> > 'program correctness' ?

Christopher Diggins wrote:

> Not directly. They are however relatively easy to type-check.
> If not, what do they offer that's special ?
> Simple semantics. Compact code. Easy to learn. Easy to implement
> efficiently. Easy to analyze and manipulate algebraically.

Well one of the most obvious reasons to want to manipulate
algebraically, must be to prove correctness.
So where's the literature with examples ?

William Tanksley, Jr wrote:

> They can because they offer (at least) one thing special: they allow
> you to build small units that are correct programs, then join those
> units together and know that the result is also a correct program.

That's what I was suspecting. Again where's the literature with
examples ?

I don't expect to find the 'magic bullet' just some tools to help
improve productivety and reliability.

For a previous poster who was asking what I think is important
in IDE's: "being able to recognise, instead of remember" is key
for me -- ie. menu driven. And while it's menu driven is can
also constrain the possible selections to those which are syntactically
valid in the 'current' context. This simple principle gives massive
increase in productivety & reliability for me.

Thanks,
== Chris Glur.

William Tanksley, Jr — 2007-05-14 15:33:36

eas lab <lab.eas@...> wrote:

> Well one of the most obvious reasons to want to manipulate
> algebraically, must be to prove correctness.

If I understand you correctly, I agree.

> So where's the literature with examples ?

I'd absolutely love to point you to a huge stack of literature with
examples and proofs. Unfortunately, all we have is a small stack, with
much of it written by people on this list. The reason is that the idea
of a "concatenative language" is almost brand new.

Manfred's Joy page will get you off to a good start. There's a lot of
it -- pick and choose what seems fun.
http://www.latrobe.edu.au/philosophy/phimvt/joy.html

Also read Kerby's exploration of combinator logic.
http://tunes.org/~iepos/joy.html

Next a little something done by someone outside of our group: Henry
Baker's excellent set of articles on "linear logic". Be sure to read
ForthStack.html ("The Forth Shall be First") -- but all these papers
are interesting.
http://home.pipeline.com/~hbaker1/

There's actually a lot more, depending on what you need and can
understand; the archives of this group will show you as well as I
could.

> I don't expect to find the 'magic bullet' just some tools to help
> improve productivity and reliability.

They're not here yet. The best thing you could do is help us produce
those tools. The second best is to help us figure out what those tools
would be like -- start talking :-)!

The Factor people are the farthest ahead in this respect. Cat is being
worked on, and I think it'll be very significant. Enchilada contains
some major advances as well. Forth has had the longest time of any
language here, so it's got a lot of tools and techniques, but there's
no unified theory behind any of them (aside from Chuck Moore's
intuition, which is not to be disrespected).

As far as IDEs go... I don't know much about that. It would be nice to
have an IDE designer here, but this isn't a language specific group,
so that's unlikely to happen. I'm sure Factor has a good IDE, since it
was written by Slava (of JEdit fame). I happen to like the minimalist
IDE of colorForth, but I doubt most people would (and even I would be
happy with more bells and whistles on that, but even there it's a fine
start).