http://atnd.org/events/6022 - ATND 初めてのCoq(yoshihiro503) 高階論理(表現力は最強) 自動証明機能(tactic)を備える プログラムと連携 仕様が証明された状態ではなく，証明されたプログラムを書くことができる tactic(小文字〜.) - Gallina式 - Vernacul…

所謂一つのKOM ですね． Scala は，ScalaCheck があっていいね． Java には，why があるよ． ネットが繋がらない．懇親会会場-- で，Coq の次の一手なんですが． ということで id:yoshihiro503 の人が居たので，Coq の次の一手(ProofGeneral の後) を聞いて…