DAGの単一始点の最短経路問題を解くアルゴリズムとか
Bellman - Fordのアルゴリズムとかの正しさの証明が非常
に面白いですね。