まあ俺ならカリーハワード同型対応に基づいて
命題=型としてのクラス外部仕様(インターフェース)作って、
次にその命題の証明として、インターフェースを満たすプログラムを実装するわけだが。

ただしプログラム合成に関しては、なんかPrologの方が多少進んでるみたいだなw