論理学の本も書いている凄腕ハッカー(≠クラッカー)が
　プログラミング＝命題証明
だって言ってたよ。