Procedure in PlusCal

I was working on Knuth's fascicle on backtracking:

https://www-cs-faculty.stanford.edu/~knuth/fasc5b.ps.gz

and I was using PLUSCAL to get a version of the algorithm B on which I could do some

experiments,

and looking at the exercise 5 that proposes to make the recursive version of the

algorithm, it came to my mind that I was once advised not to use the procedure

facilitiy of PLUSCAL. (see p. 26)

https://lamport.azurewebsites.net/tla/c-manual.pdf

but to use the TLAPLUS mathematical constructs instead (sets, mathematical functions etc.)

It was a very good piece of advice. It amounts to replacing a procedure by its postcondition.

Mathematically speaking, there is nothing wrong with this way of doing. And practically

speaking this prevents the burden of stacks and labels generated by procedures. (It leads

to program that are less simple to prove.)

So the rule is: don't use procedures, work through each algorithm in isolation.

However there is one case where procedures are required: recursive algorithms.

I think it is the only legitimate case.

And since there is always one way to turn a recursive algorithm into a non-recursive

with old good loops and so on, this legitimate case is of little use.

But to work on Knuth's exercise 5, use procedures.