証明の証明

なんというか、プログラムの正しさを証明しようとすると、その証明の正しさを証明して欲しくなる。人手で証明すると間違えるんですよね。まぁ、はまったわけです。てか、プリントが間違ってる・・・。どこまで自動化できるのか。定理証明は最近流行ってるらしいですが。

で、なぜ今更 Hoare logic なんてやっているのか。ひさびさに宿題のレポートを書いた次の日の感想。