プログラムと証明

昔書いた、Hoare Logic を見直してたんですが

　　メタで証明を切り分ける

ってやってたんだが、最近、証明ばっかりやってたので、

　　切り分けると書きづらい

となってきた。Agda だと命題だけ書いて証明後回しで良いので、無理に切り分けなくて良いのではとなってます。

という話をOS研究会でやるのか?!