# WHY: concatenative languages ?

## chris glur — 2007-05-07 16:19:48

    I came to this forum via a chaotic search for methods to formally prove

    program/algorithms correct.  The vague hope is reinforced by what I

    recently read in:

    http://www-rocq.inria.fr/~dpotop/potopMemocodeBook.pdf

     > The underlying synchronous model also allows the use of the well-studied

    > functional verification techniques developed  for synchronous circuits,..

     I speculate/hope that the following is true and will bring me closer to

    my destination;

    -  functional 'formatted' algorithms can be manipulated to prove

      correctness;

    - concatenative format can help the 'mathematical manipulations'

      to prove correctness.

    Is there any truth in this speculation/hope ?

    And if so, can someone point me to text[s] which deals with the big

    picture level of my goal.

    I don't want to just analyse another way of saying "hello world".

    Thanks,

    == Chris Glur.