"TDD is dead. Long live testing" の元ネタについての英文解釈的雑談 - 亀岡的プログラマ日記
話題になりましたね、"TDD is dead"。 TDD is dead. Long live testing. (DHH) そしてやっとむさんが素晴らしい日本語訳を公開していただきました。 TDDは死んだ。テスティングよ栄えよ。 by DHH @やっとむでぽん 今回、内容の話はしません（ぉ。英語の話をします。*1 このタイトル、"TDD is dead. Long live testing."、なんか気になりません？と言うか日本人的には意味がちょいとわからない。。。 実は、これには元ネタがあります。 英辞郎をどうぞ。 the king is deadの意味・用例｜英辞郎 on the WEB：アルク The king is dead; long live the king! 王様は亡くなった。王様万歳！ 個々人としての王が死去しても、王制は継続するという意味。王が「死んだ」と言ったすぐあ
なぜCoqが重要か
結論 最強のプログラム検証器 最強の関数型言語 最強のプログラム検証器 Coqは最強の表現力を持つ仕様記述言語を使う 仕様記述言語は検証したいこと を記述するための言語 表現力は検証器によって全然違う 表現できる範囲が、検証器の限界 Coqのそれは高階述語論理 ← 最強 最強のプログラム検証器 Coqを使うためにはPhDが必要? 高校生でも練習すればできる (c.f. プログラミングCoq) 最強のプログラム検証器 証明を人間が与えるのが大変？ タクティックによる自動化はOCamlでいくらでも可能 型チェッカはタクティックと独立なので安全 既にomegaなどの自動証明アルゴリズムを実装したタクティックあり 最強の関数型言語 Coqは(型の表現力が)最強の関数型言語 型の表現力が最強 型推論は完全ではない 停止性は保証しなければならない 注意: ここでの関数型言語とは (ラムダ計算を基礎とし
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
