プログラミング好きの備忘録

関数型言語とか、証明とか

ソフトウェアの基礎

今日は8月に入って初めての、予定がまったく入っていない日でした。
自分で設定した、夏休みの課題を推めることにしました。

・TAPL
読み始めると(遅々ながら)のめり込むことができる。でも、とっかかりが難しい。

というわけで、今日はTAPLは進まなかった(意志を強く持て!)

・ソフトウェアの基礎
TAPLの作者が書いた本、の翻訳版。媒体は電子書籍。Coqの入門書。
これを進めました。主に写経です。

今日の進捗は15ページから初めて64ページまで。文字が大きいせいもあって、本全体では1134ページ


学んだこと
・列挙型の宣言
・simpl, intros, rewrite, destruct, case, inductionなど。このへんは前にCoq触ったときに使ったことがある。

レベル3以上の練習問題が解けなかった。日を改めて、あきらめずに再挑戦しよう。


#Coqはおもしろいんだけど、こればっかやってるとJavaが身につかないんだよな...