LL魂のLTがかっこいいことになっている件

http://ll.jus.or.jp/2007/show/Event/Session#H-dh4f51

Coq定理証明という選択肢

Lightweightじゃないどころか、言語ですらないwww