Re: [stack] Re: How the Interpreter Works

Chris,

Perhaps a comparison to another functional language, Haskell,
would be useful.

Haskell offers many opportunities for the use of formal
methods, since it is referentially transparent.   This property
allows you to manipulate Haskell code in the same way you
can manipulate a set of equations.

An example of Haskell's use in this manner is in the paper
"The Design of a Pretty Printing Library", by John Hughes.
(http://citeseer.ist.psu.edu/hughes95design.html) He begins
with a simple design and elaborates it through algebraic
transformations of the Haskell source code until he arrives at
a sophisticated, efficient design.  The final product is related
to the initial product through these transformations.

But perhaps that's not precisely what you mean by formal
methods.  Another Haskell-based approach is embodied in
the library QuickCheck.  Here you write specifications for
your code in the embedded domain-specific language
QuickCheck, which is itself a Haskell combinator library.
Then QuickCheck automatically generates test cases to check
that your Haskell code obeys your specifications.  This is more
than unit testing -- it's a way to develop formal specifications
and working code simultaneously.  See the paper "Specification-
based testing with QuickCheck" at
http://www.math.chalmers.se/~koen/pubs/entry-fop-quickcheck.html

But QuickCheck is still not a proof.  It's just looking for
counter-examples to your specifications.  And the "places" it
looks are random, at that.  The Alloy tool (not related to Haskell)
is like QuickCheck, in that it looks for counter-examples, but it
does an exhaustive check all the way up to a maximum size.
See http://alloy.mit.edu.

But that's still not a proof of correctness.  Once you begin asking
for real proofs, you're right, it's very difficult.  Progress has been
slow.  The so-called lightweight formal methods above give
confidence that your code is correct, but they are not proofs.

However... proofs using Haskell are far easier than proofs using,
say, C.  Referential transparency is the key.  And proofs have
been done on practical Haskell libraries.  See Graham Hutton,
http://www.cs.nott.ac.uk/~gmh/bib.html, for a few examples.

So, back to concatenative programming.  Most if not all proofs
done in Haskell rely on the type system.  The Haskell type
system enforces referential transparency.  Cat is the only stack
language I know of that has a type *system* that might be up
to the task.  Yet I hear people on this list claiming that the
property of concatenativity alone will get you to a place where
formal methods become practical.  What about it?

-Rod


>  > I know a bit about compilers/interpret
ers and it's not clear

>  > why I would want to analyse another one. I was hoping that

>  > 'concatinative methods' would lead towards a formal

>  > [mathematical like] way of anlysing algorithms and/or

>  > proving code correctness. Does it ?


Christopher Diggins wrote;

>  In general the concatenative approach greatly simplifies reasoning

> about algorithms and code. It also simplifies automated translation,

> analysis, compilation, and optimization. Check out Manfred von Thun's

>  writing about algebraic manipulation of concatenative code

>(
http://www.latrobe.
edu.au/philosoph
y/phimvt/
joy/j04alg.
html
 ).

>It is common for most compilers to reduce code to a point-free form

>  (e.g. nameless) before conducting further analysis, which I think

>  testifies to the usefulness of point-free forms (concatenative or

>  otherwise). The fact that call-by-push-
value semantics

> (
http://citeseer.
ist.psu.edu/
234600.html
 )

> subsumes call by name and  call by value semantics may also

> indicate that stack-based approaches  are perhaps a more

> general formalism than either of them.


As previously stated I'm aware of Backus' and McCarthy's

promotions of functional programming for facilitating formal methods

of correctness proof.  But that's decades ago, and I've never seen that

anything usable came of it.  It reminds me of these blokes that spend

every weekend polishing their vehicles, but have never made a 'journey'!


The first part of joy/j04alg.html looks like interesting manipulations,

but no indication for me that it will achieve 'formal methods'.


What I need to see is a 'hello world', as a proof of concept.

My related rant below, hopefully further explains why I'm reluctant to

start a journey which won't reach a profitable destination.


Thanks,


== Chris Glur.


PS. rant will be enlarged in later post.

WebBased gmail is difficult to manage ?

And spammers drove me from normal mailer.