[stack] WHY: concatenative languages ?

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.