学生の発表練習

Agda なんで難しいんですけどね。

　　ソースコードに行番号

うーん、好きな人がいるのは知ってるのだが、初出のプログラミング言語に行番号は辛い感じ。さらに、

　　改行してコメント行

それは、ちょっとないかな。Agdaなので「実行結果」みたいなものがないので、それをコメント行に書きたいのはわかるけど。

でも、その辺りは地の文にしようよ。

なかなか聞いてくれる人の気持ちになって資料を作るというのは難しい。自分でも自分勝手になってしまうしな。

でも、今年のM2は、Agda で codeGear の Hoare Logic based Proof を Soundness / Termination 込みで書けたので成果はあった感じです。

さきがけのプロポーザルに書いたのがようやっと書けて良かった。