ラムダノート(LamdaNote)社の新刊「Goならわかるシステムプログラミング」「定理証明手習い」。テスト駆動開発(TDD)の限界、Formal Methods(形式仕様記述、形式手法)のことも。 ― 2017年11月01日 00時40分07秒
ASAHIネット(http://asahi-net.jp )のjouwa/salonから。
---
元オーム社、現在、ラムダノート(LambdaNote)社の鹿野さんのツイートを偶然みた。
https://twitter.com/golden_lucky/status/924922453477924864
『Goならわかるシステムプログラミング』と『定理証明手習い』、初回があっという間に品切れになっていた新宿紀伊国屋さんにも再入荷したと思われるので、見かけたら教えてください(そしてぜひレジへ)
17:54 - 2017年10月30日
よっしゃ、ご祝儀隊、出動!
さっそく、新宿紀伊国屋書店に行ったら、2つが並べて平積みになっていた。即ゲット。
もう読まなくてもいいです。どっちもいいに決まっている。手元にあるだけで満足。\(^O^)/
読めよ!
https://www.lambdanote.com/blogs/news/go
新刊『定理証明手習い』と『Goならわかるシステムプログラミング』の発売を開始しました!
2017年10月19日
ラムダノートは、ほかにもRubyでRubyを作ってプログラミング言語を学ぶ本も出しています。
https://www.amazon.co.jp/exec/obidos/ASIN/4908686017/showshotcorne-22/
RubyでつくるRuby ゼロから学びなおすプログラミング言語入門 テキスト – 2017/3/31
遠藤侑介 (著)
https://www.lambdanote.com/products/ruby-ruby
RubyでつくるRuby ゼロから学びなおすプログラミング言語入門
Rubyインタプリタを自作してプログラミングを始めよう!
関連:
http://iiyu.asablo.jp/blog/2017/03/29/8425028
純粋関数型データ構造、型システム入門、Ruby でつくる Ruby、鹿野さん、高尾さんのラムダノート
■Goならわかるシステムプログラミング
https://www.lambdanote.com/collections/go
『Goならわかるシステムプログラミング』
Go言語による新時代のコンピュータシステム入門
「Goならわかるシステムプログラミング」は、電子書籍は、売ってないみたい。
この本は、ウェブでの連載をベースに加筆、修正して紙書籍にしたもの。
http://ascii.jp/elem/000/001/235/1235262/
Goならわかるシステムプログラミング
このウェブ連載を全部読まなくても、本書の目次を見ただけで、いいよ、これと思う。
あなたも買いなさい。
押し売りすんなって。
関連:
http://iiyu.asablo.jp/blog/2016/10/01/8207327
プログラミング言語Go、みんなのGo言語、改訂2版 基礎からわかる Go言語
http://iiyu.asablo.jp/blog/2016/04/06/8066132
Effective Python, Pythonチュートリアル第3版, Go言語によるWebアプリケーション開発, スターティングGo言語
http://iiyu.asablo.jp/blog/2016/01/14/7990070
Go言語によるWebアプリケーション開発
http://iiyu.asablo.jp/blog/2014/08/28/7423307
プログラミング言語Go, Mastering Concurrency in Go
Goつながりで、こんなのも。
http://iiyu.asablo.jp/blog/2016/07/27/8140232
ポケモンGOより、栄養があって夏バテにいいらしいわ
http://iiyu.asablo.jp/blog/2016/07/26/8139633
ポケモンGO、鹿児島は特別バージョンらしいわ
■定理証明手習い
https://www.lambdanote.com/collections/littleprover
『定理証明手習い』
プログラムの正しさは証明できる。定理証明へ踏み出すための最高のガイドブック
--- ここから ---
あるプログラムが、考えられるあらゆる入力に対して誤った動作を引き起さないことは、テストを書いても確かめられません。それを確かめるには、公理と式の等価な書き換えだけで恒真を導いたり、再帰的なプログラムの構造に照した帰納法による証明が必要です。
--- ここまで ---
で思い出した。
プログラムの正しさは証明する手助けになるのが、Formal Methods(形式仕様記述、形式手法)。
テスト駆動開発(Test Driven Development, TDD)がいいというが、ぼくは、あんまりねえと思う。
上記と同じ理由で、プログラマが思いついた条件だけはテストできるが、数学的、論理学的に正しさを証明できるわけではないから、テスト漏れがいくらでも考えられるわけ。
TDDは、現場の知恵的な実践的な手法ではあっても、Formal Methodsに比べると限界があると思っている。
Formal Methodsも、それが直接、現実のプログラムとして使えるものではないので、現実のプログラミング言語で動くものは書かないといけないというハンデはあるけれど。
アマゾンのウェブサービス(AWS, Amazon Web Services)は、あるときから、Formal Methodsを使って作られている、という話をブログに書いたと思ったら、書いてないね。数年前の話。そのうち、書くね。
そしたら、こんなツイートがあったので、反応した。
https://twitter.com/golden_lucky/status/922730533771079680
定理証明はなんでふつうの開発で話題になってないのですか、というFAQにはちょっと詰まってしまったので、適切な返答ありませんか
https://twitter.com/shownakamura/status/925278039839141888
Fomal Methods(形式的仕様記述、形式手法)は、開発の現場で話題になることはあるが、ふつうの開発ではどうかな。Lispがふつうの開発で話題にならないのと同じ? 実は、アマゾンのAWSはあるときからFormal Methodsを使って作られている。いずれ書く。
その他、Formatl Methodsについては、何度も書いているので、上の検索窓に「Formal Methods」「形式仕様記述」と入れて検索してください。
さて、「定理証明手習い」は、PDF版はある。
「定理証明手習い」は、紙書籍を買った人にも、特別価格でのPDF販売があるという。
https://www.lambdanote.com/blogs/news/article-2
書店などで『定理証明手習い』紙書籍をお買い上げ頂いた方へ、特別価格でPDF版を提供します
2017年10月27日
上記のニュースリリースなど見ずに、新宿紀伊国屋書店に走ったので、「定理証明手習い」って何だろうと思っていたら、新宿紀伊国屋書店で、手にとってすぐわかった。
「The Little Prover」の日本語版だ。
https://www.amazon.co.jp/exec/obidos/ASIN/0262527952/showshotcorne-22/
The Little Prover (MIT Press) (英語) ペーパーバック – 2015/7/10
Daniel P. Friedman (著), Carl Eastlund (著), Duane Bibby (イラスト), J Strother Moore (はしがき), Matthias Felleisen (あとがき)
ペーパーバック
¥ 4,665
¥ 2,729 より 5 中古品の出品
¥ 4,407 より 18 新品
著者のDaniel P. Friedmanは、「The Little Schemer」(日本語版は「Scheme手習い」)が好評で、以後、Scheme系とThe Little XXXを何冊も出すが、それについては、関連をどうぞ。
この日本語版の制作過程がすごい。PDFからXMLにしてLaTeXにしてPDFにしている。
鹿野さんと三重大学の奥村晴彦先生とのツイッターでのやり取り。奥村先生は、LaTeXでも有名。
--- ここから ---
keiichiro shikano λ♪ @golden_lucky 20 時間20 時間前
ぼくにとってLaTeXの文書はXMLから生成するものなので、.texを手書きすると、1行目に\begin{documentclass}とか書いて固まることがあります。
Haruhiko Okumura @h_okumura 20 時間20 時間前
XMLは何から生成するのですか?
keiichiro shikano λ♪ @golden_lucky 20 時間20 時間前
PDFとか、InDesignとか、もしくはHTMLです。
Haruhiko Okumura @h_okumura
返信先: @golden_luckyさん
PDF→XML→LaTeX→PDF円環の理
18:19 - 2017年10月30日
keiichiro shikano λ♪ @golden_lucky 19 時間19 時間前
返信先: @h_okumuraさん
実際、『定理証明手習い』は、その円環でした(原著PDFしかない、生LaTeXだとブラウザでプレビューできない、などの理由から)
Haruhiko Okumura @h_okumura 19 時間19 時間前
!すごい!
--- ここまで ---
関連:
http://iiyu.asablo.jp/blog/2010/10/06/5387189
新しくなった「Scheme手習い」
http://iiyu.asablo.jp/blog/2008/08/30/3723146
CTM, Mozart, Oz情報
---
元オーム社、現在、ラムダノート(LambdaNote)社の鹿野さんのツイートを偶然みた。
https://twitter.com/golden_lucky/status/924922453477924864
『Goならわかるシステムプログラミング』と『定理証明手習い』、初回があっという間に品切れになっていた新宿紀伊国屋さんにも再入荷したと思われるので、見かけたら教えてください(そしてぜひレジへ)
17:54 - 2017年10月30日
よっしゃ、ご祝儀隊、出動!
さっそく、新宿紀伊国屋書店に行ったら、2つが並べて平積みになっていた。即ゲット。
もう読まなくてもいいです。どっちもいいに決まっている。手元にあるだけで満足。\(^O^)/
読めよ!
https://www.lambdanote.com/blogs/news/go
新刊『定理証明手習い』と『Goならわかるシステムプログラミング』の発売を開始しました!
2017年10月19日
ラムダノートは、ほかにもRubyでRubyを作ってプログラミング言語を学ぶ本も出しています。
https://www.amazon.co.jp/exec/obidos/ASIN/4908686017/showshotcorne-22/
RubyでつくるRuby ゼロから学びなおすプログラミング言語入門 テキスト – 2017/3/31
遠藤侑介 (著)
https://www.lambdanote.com/products/ruby-ruby
RubyでつくるRuby ゼロから学びなおすプログラミング言語入門
Rubyインタプリタを自作してプログラミングを始めよう!
関連:
http://iiyu.asablo.jp/blog/2017/03/29/8425028
純粋関数型データ構造、型システム入門、Ruby でつくる Ruby、鹿野さん、高尾さんのラムダノート
■Goならわかるシステムプログラミング
https://www.lambdanote.com/collections/go
『Goならわかるシステムプログラミング』
Go言語による新時代のコンピュータシステム入門
「Goならわかるシステムプログラミング」は、電子書籍は、売ってないみたい。
この本は、ウェブでの連載をベースに加筆、修正して紙書籍にしたもの。
http://ascii.jp/elem/000/001/235/1235262/
Goならわかるシステムプログラミング
このウェブ連載を全部読まなくても、本書の目次を見ただけで、いいよ、これと思う。
あなたも買いなさい。
押し売りすんなって。
関連:
http://iiyu.asablo.jp/blog/2016/10/01/8207327
プログラミング言語Go、みんなのGo言語、改訂2版 基礎からわかる Go言語
http://iiyu.asablo.jp/blog/2016/04/06/8066132
Effective Python, Pythonチュートリアル第3版, Go言語によるWebアプリケーション開発, スターティングGo言語
http://iiyu.asablo.jp/blog/2016/01/14/7990070
Go言語によるWebアプリケーション開発
http://iiyu.asablo.jp/blog/2014/08/28/7423307
プログラミング言語Go, Mastering Concurrency in Go
Goつながりで、こんなのも。
http://iiyu.asablo.jp/blog/2016/07/27/8140232
ポケモンGOより、栄養があって夏バテにいいらしいわ
http://iiyu.asablo.jp/blog/2016/07/26/8139633
ポケモンGO、鹿児島は特別バージョンらしいわ
■定理証明手習い
https://www.lambdanote.com/collections/littleprover
『定理証明手習い』
プログラムの正しさは証明できる。定理証明へ踏み出すための最高のガイドブック
--- ここから ---
あるプログラムが、考えられるあらゆる入力に対して誤った動作を引き起さないことは、テストを書いても確かめられません。それを確かめるには、公理と式の等価な書き換えだけで恒真を導いたり、再帰的なプログラムの構造に照した帰納法による証明が必要です。
--- ここまで ---
で思い出した。
プログラムの正しさは証明する手助けになるのが、Formal Methods(形式仕様記述、形式手法)。
テスト駆動開発(Test Driven Development, TDD)がいいというが、ぼくは、あんまりねえと思う。
上記と同じ理由で、プログラマが思いついた条件だけはテストできるが、数学的、論理学的に正しさを証明できるわけではないから、テスト漏れがいくらでも考えられるわけ。
TDDは、現場の知恵的な実践的な手法ではあっても、Formal Methodsに比べると限界があると思っている。
Formal Methodsも、それが直接、現実のプログラムとして使えるものではないので、現実のプログラミング言語で動くものは書かないといけないというハンデはあるけれど。
アマゾンのウェブサービス(AWS, Amazon Web Services)は、あるときから、Formal Methodsを使って作られている、という話をブログに書いたと思ったら、書いてないね。数年前の話。そのうち、書くね。
そしたら、こんなツイートがあったので、反応した。
https://twitter.com/golden_lucky/status/922730533771079680
定理証明はなんでふつうの開発で話題になってないのですか、というFAQにはちょっと詰まってしまったので、適切な返答ありませんか
https://twitter.com/shownakamura/status/925278039839141888
Fomal Methods(形式的仕様記述、形式手法)は、開発の現場で話題になることはあるが、ふつうの開発ではどうかな。Lispがふつうの開発で話題にならないのと同じ? 実は、アマゾンのAWSはあるときからFormal Methodsを使って作られている。いずれ書く。
その他、Formatl Methodsについては、何度も書いているので、上の検索窓に「Formal Methods」「形式仕様記述」と入れて検索してください。
さて、「定理証明手習い」は、PDF版はある。
「定理証明手習い」は、紙書籍を買った人にも、特別価格でのPDF販売があるという。
https://www.lambdanote.com/blogs/news/article-2
書店などで『定理証明手習い』紙書籍をお買い上げ頂いた方へ、特別価格でPDF版を提供します
2017年10月27日
上記のニュースリリースなど見ずに、新宿紀伊国屋書店に走ったので、「定理証明手習い」って何だろうと思っていたら、新宿紀伊国屋書店で、手にとってすぐわかった。
「The Little Prover」の日本語版だ。
https://www.amazon.co.jp/exec/obidos/ASIN/0262527952/showshotcorne-22/
The Little Prover (MIT Press) (英語) ペーパーバック – 2015/7/10
Daniel P. Friedman (著), Carl Eastlund (著), Duane Bibby (イラスト), J Strother Moore (はしがき), Matthias Felleisen (あとがき)
ペーパーバック
¥ 4,665
¥ 2,729 より 5 中古品の出品
¥ 4,407 より 18 新品
著者のDaniel P. Friedmanは、「The Little Schemer」(日本語版は「Scheme手習い」)が好評で、以後、Scheme系とThe Little XXXを何冊も出すが、それについては、関連をどうぞ。
この日本語版の制作過程がすごい。PDFからXMLにしてLaTeXにしてPDFにしている。
鹿野さんと三重大学の奥村晴彦先生とのツイッターでのやり取り。奥村先生は、LaTeXでも有名。
--- ここから ---
keiichiro shikano λ♪ @golden_lucky 20 時間20 時間前
ぼくにとってLaTeXの文書はXMLから生成するものなので、.texを手書きすると、1行目に\begin{documentclass}とか書いて固まることがあります。
Haruhiko Okumura @h_okumura 20 時間20 時間前
XMLは何から生成するのですか?
keiichiro shikano λ♪ @golden_lucky 20 時間20 時間前
PDFとか、InDesignとか、もしくはHTMLです。
Haruhiko Okumura @h_okumura
返信先: @golden_luckyさん
PDF→XML→LaTeX→PDF円環の理
18:19 - 2017年10月30日
keiichiro shikano λ♪ @golden_lucky 19 時間19 時間前
返信先: @h_okumuraさん
実際、『定理証明手習い』は、その円環でした(原著PDFしかない、生LaTeXだとブラウザでプレビューできない、などの理由から)
Haruhiko Okumura @h_okumura 19 時間19 時間前
!すごい!
--- ここまで ---
関連:
http://iiyu.asablo.jp/blog/2010/10/06/5387189
新しくなった「Scheme手習い」
http://iiyu.asablo.jp/blog/2008/08/30/3723146
CTM, Mozart, Oz情報
最近のコメント