I've lately been trying to write code with no recursion - as in able to be implemented with each function having a variable indicating where to return to, no implicit stack in sight. (Statically-determinable stack size, to put it another way.)

It took me a bit to get the hang of, but I'd argue that it ends up being easier in the long run. Far easier to change the priority operator on your queue than trying to reason what behavior different orders of recursion get you, for example.

Ditto with graph search algorithms. It's enlightening to teach graph search algorithms as a single algorithm with a queue, where changing the priority gives you Dijkstra's algorithm (least cost first), DFS (LIFO), BFS (FIFO), A* (current cost + underestimating huristic of cost left), or whatever. Also easy to show that A* degenerates into Dijkstra's algorithm when you use a null heuristic (i.e. a heuristic that returns a constant) if you teach them as variants of the same algorithm.

which likely sums up what Lamport is trying to get across - express your work equationally, determine properties and generally understand what you're dealing with and then later, you can 'compile your equations' down to a particular implementation. from my own practice, i've found that it is much easier to reason about equations and reflect it down into code than to try and reason about the code