Yes, you have it exactly right, including the usage of non-local control flow to interrupt and restart the search. [0] is another implementation in an imperative language.

[0] https://github.com/monte-language/typhon/blob/master/mast/fu...