Question about the formal proof of the inorder traversing
It is definitely possible to analyze this algorithm using Hoare triples. The first step would be to replace the VISIT procedure calls with some more reasonable accounting mechanism, say a list that lists the visited nodes in order. You then define formally what a binary tree is and what an inorder traversal is, something along the following lines:

Tree = Leaf N | Node N LTree RTree
Inorder(Leaf N) = N
Inorder(Node N LTree RTree) = Inorder(LTree) || N || Inorder(RTree)


Here N is the "name" of the node, and || is list concatenation. Armed with these notions, it is an exercise to construct the required Hoare triples. You will probably need to come up with even more notions (for example, you will need to explain what the contents of the stack are when a node P is popped).

What do we gain from this exercise? Do we understand the algorithm any better? Probably not. But we understand how to reason precisely about algorithms, something which is useful if you plan on doing software verification or programming language theory, areas forming the so called "Theory B". If you're more of a "Theory A" type (algorithms and complexity) then, like me, you will find such exercises somewhat beside the point.