Re: [stack] Re: How the Interpreter Works

Rodney D Price <[email protected]> wrote:
>  Perhaps a comparison to another functional language, Haskell,
>  would be useful.

Great examples -- thanks.

>  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.

There are systems designed to allow formal proofs to be embedded with
regular code. Interestingly, the only one I'm familiar is for a
language that isn't referentially transparent, Ada. (SPARK Ada,
specifically.)

>  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?

Well, a type system is itself a formal method; it's just a subset of
more extensive automated proofs. Fifth is another concatenative
language that, in addition to an inferenced type system, has an
effects system. I don't know whether its effects system is influenced
or benefitted by its concatenativity.

I do know of one concatenative language, strongForth, that added a
complete strong type system (excluding type inference) that runs at
the same time as the compiler's linear-time parse. That (linear time
typechecking) was made simpler by concatenativity (although I don't
know that it's impossible without it).

>  -Rod

-Wm