ソフトウェアの形式手法では、なにかしら論理の力の借ります。論理には、ウンザリするほどの種類がありますが、コンピューティングに利用するなら、ホーア論理が一番基本的で一番役に立つものだと思います。ホーア論理の圏論的な定式化というと、アブラムス…

サッカーの録画を見ながら：次男：「左サイドあいてるー」父親：「…」次男：「うーん、もっとプレッシャーかけないと」父親：「…」次男：「そうそう、コンパクトに」父親：「…」次男：「おっとフェイント、ロコモティブだ」父親：「君さ、随分と難しいこと知…