ASAHIネット(http://asahi-net.jp )のブログサービス、アサブロ(https://asahi-net.jp/asablo/ )を使っています。
---
　もう早く書かないから、明日まで。
　翔泳社が電子書籍を50%ポイント還元セール中。
　ま、そのうち、また、やるだろうから、その時でもいいけど。

https://www.amazon.co.jp/exec/obidos/ASIN/4798169161/showshotcorne-22/
実践TLA+ 単行本（ソフトカバー） – 2021/9/15
Hillel Wayne (著), 株式会社クイープ (翻訳, 監修)

https://www.amazon.co.jp/exec/obidos/ASIN/B09BJ44451/showshotcorne-22/
実践TLA+ Kindle版
Hillel Wayne (著), 株式会社クイープ (翻訳, 監修) 形式: Kindle版

　翔泳社にある紹介。PDFはここで買える。
https://www.seshop.com/product/detail/24750
実践TLA+【PDF版】

　ランポート先生(Leslie Lamport)といえば、LaTeXの作者であることを知っている人も多いと思うが、TLA+のような仕事もやっているし、フォールトトレラントや分散環境のビザンチン将軍問題が有名。
　すごい人は、何をやってもすごいということ。
https://ja.wikipedia.org/wiki/ビザンチン将軍問題

　数年前までブロックチェーン芸者になってウソや筋の悪い話を書いていた経済学者、野口悠紀雄のトンデモブロックチェーンの話も、この辺に関係する。
　ダイヤモンド社、東京経済新報社、日本経済新聞社、文藝春秋社など、文系、ビジネス系出版社は、野口悠紀雄の出来の悪さがわからないから、記事を書かせたり、本を出したりしているんだよね。
　こういう文系出版社の科学や技術に対するリテラシーの低さが、日本の失われた10年、20年、30年、さらに永遠(苦笑)の大きな要因だと思っている。

　何度も書くが、SuicaやPasmoといったソニーのフェリカネットワークスのFeliCaを使った電子カードは、フォーマルメソッドで開発された。

http://iiyu.asablo.jp/blog/2018/10/30/8985607
テスト駆動開発(TDD)より、形式手法(フォーマルメソッド、形式仕様記述、Formal Methods)。九州大学(九大)の荒木啓二郎先生が、熊本高等専門学校(熊本高専)の校長に！記念、形式手法とネットワーク技術シンポジウム
から
--- ここから ---
　世の中、まだ、テスト駆動開発(TDD)しか知らず、形式手法(フォーマルメソッド、Formal Methods)を知らない人が多い。
　以前書いたけど、Suicaやパスモなど、ソニーのフェリカネットワークスのFeliCaを使ったICカードは、形式手法を使って作られたし、アマゾンのサービスも、形式手法を使って作るようになったという話もある。この辺、時間があったら書こうと思って、もう２，３年経っている。
　ちょっとだけ書くと。
　TDDは、結局、プログラマが書いた場合しかテストできないので、バグは残る。形式手法は、数学的にプログラムの正しさを証明する。だから、正しいと証明された部分にバグはない。
　ソフトウェア開発の現場の技術レベルを考えれば、実践できるのは、大体、テスト駆動開発(TDD)が精一杯という話もあるけど、TDDしか知らない人、TDDの限界を感じている人は、形式手法を学ぶのもいいと思いますよ。
--- ここまで ---

　FeliCaの開発のこと、開発を主導した栗田太郎さんの話などは、
http://iiyu.asablo.jp/blog/2010/07/29/5254545
VDM++によるオブジェクト指向システムの高品質設計と検証
を読んでください。
　栗田さんは、FeliCaの仕事を基に博士号を取得したので、ご同慶の至り。

　もう5年以上前かな。Amazon AWSに適用した事例の論文があって、面白かったのは、現場のエンジニア、プログラマは数学や論理学に抵抗があるから、検証や証明といった用語は使わず、網羅的なテストツールだという言い方をしてAmazon内に普及させたという話。
　その後、ちょっと調べたら、あの論文を書いた人たちは、たしかOracleだったかな、もう別の会社に移っていた。
　あった。2014年だね。
https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf
Use of Formal Methods at Amazon Web Services
Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, Michael Deardeuff
Amazon.com
29th September, 2014
　「Exhaustively testable pseudo-code」だから、「網羅的なテストツール」ではなく、「網羅的なテストができる擬似コード」だね。

　フォーマルメソッドの第一人者、九州大学(当時)の荒木啓二郎先生の2010年のの論文。
https://www.jstage.jst.go.jp/article/secjournal/6/2/6_104/_pdf
ソフトウェア開発現場への形式手法導入
—形式手法適用の実経験から得られた知見—
形式手法人材育成WGリーダー
九州大学　大学院システム情報科学研究院　教授　工学博士
荒木　啓二郎

https://codezine.jp/article/detail/10505
「形式手法」の“論理の力”による開発効率と品質の向上事例
トップエスイーからのアウトカム ～ ソフトウェア工学の現場から 第7回
石川 冬樹（国立情報学研究所）[著]
2017/11/07 14:00

https://dev.classmethod.jp/articles/what-is-tlaplus/
[TLA+] TLA+と形式仕様言語 [目的と準備]
小室 啓

https://qiita.com/autotaker1984/items/52cd65486a3186af080b
形式手法はなぜ流行っていないのか
2021年03月25日に投稿
2021年03月27日に更新

関連：
http://iiyu.asablo.jp/blog/2018/10/30/8985607
テスト駆動開発(TDD)より、形式手法(フォーマルメソッド、形式仕様記述、Formal Methods)。九州大学(九大)の荒木啓二郎先生が、熊本高等専門学校(熊本高専)の校長に！記念、形式手法とネットワーク技術シンポジウム
http://iiyu.asablo.jp/blog/2017/11/01/8718707
ラムダノート(LamdaNote)社の新刊「Goならわかるシステムプログラミング」「定理証明手習い」。テスト駆動開発(TDD)の限界、Formal Methods(形式仕様記述、形式手法)のことも。
http://iiyu.asablo.jp/blog/2011/12/28/6266615
形式手法導入パイロット教育コース
http://iiyu.asablo.jp/blog/2011/09/19/6107007
文章が駄目ならシステムも駄目、形式仕様記述(フォーマルメソッド)のことも
http://iiyu.asablo.jp/blog/2011/02/04/5662037
仕様記述言語Alloy, Software Abstractionsの翻訳がオーム社から出そう＼(^O^)／
http://iiyu.asablo.jp/blog/2010/09/18/5354010
関数プログラミングの楽しみ
http://iiyu.asablo.jp/blog/2010/07/29/5254545
VDM++によるオブジェクト指向システムの高品質設計と検証
http://iiyu.asablo.jp/blog/2010/07/29/5254556
フォーマルメソッド(形式仕様記述、Formal Methods)の教科書
http://iiyu.asablo.jp/blog/2006/08/20/491884
形式仕様記述(フォーマルメソッド、Formal Methods)
http://iiyu.asablo.jp/blog/2010/08/10/5277689
地球なう。おれのサンプルリターンは大成功＼(^O^)／