結論めいたもの

Ｃ言語のような文法の言語でも書けますけれども、条件分岐ではなく、lispにおけるcondのような「パターンマッチングによる関数呼び出しのオーバーライド」→状態遷移図と考えることにより、

• 条件のチェック
• 関数の中身のチェック

を分離することで、プログラムが終了するかどうかの判定／証明が容易になる、、、、気がします。

アルゴリズムが正しいかどうかの証明は　また別の話ですけれども。