Hi I think that it is interesting that there is a programmer in the UK that produces one of the few provable program products for correctness ( to specification ) that meet some standard ( I forget which ) and his programs are all done in Forth ( that uses two stacks ). My understanding is that most of the reason he can produce this is that the language it self is built and verified by him and that even though there are stacks, use is usually more controlled and maximum depths can be calculated. Most Forth processes are done with cooperative tasking rather than the more random effects of preemptive. This also means better predictability. The other part is that Forth programs tend to be highly factored. This means that hierarchical verification is more practical. It is easier to understand the range of valid inputs for each piece and how those effect the next level up. He writes program for such things as subway control systems. His products need to meet tight controls that need to be absolutely correct or people die. Strange that he would use a language that not only uses a stack but uses two stacks and still produces verifiable results. He considers that choice to be a most important one. Dwight