過去・現在・未来

「はじめてのCoq」ハンズオンにお申込みいただいてありがとうございます。 当日の演習課題部分（講義資料は含まれていません）を、GitHubに公開しました。 https://github.com/maruyama097/coq-tutorial どんな感じの演習課題なのかは、GitHubで確認できると思います。 git clone  https://github.com/maruyama097/coq-tutorial  していただければ、 ご自身のマシン上に展開できると思います。 ハンズオン、coqとcoq−jupyter（この資料は、coq−jupyterの上で動きます）のインストールの手間を省いて、クラウドとブラウザー・ベースでやろうと思っていたのですが、作業をしていて、あることに気づきました。今更ですが。 演習課題配っても、coqとcoq−jupyterをインストールしていない限りは、この資料動かないですね。（GitHubでは、イメージは見れるのですが、課題は動きません。） それに、ハンズオンの当日以外には、coqとcoq−jupyterの環境を、持っていない人は、資料を復習することも、自分でcoqの学習を進めることもできないですね。 ハンズオンのやり方を変えようと思っています。今回のハンズオンを機会に、自分のマシン上でcoqとcoq−jupyterが動くようにするのがいいのではと考え始めています。お時間があったら、coqとcoq−jupyterのインストールをおためしください。 一番簡単な、coqとcoq−jupyterのインストールの方法は、anacondaを使う方法だと思います。まず、anaconda をインストールします。次の資料が参考になると思います。 「Anaconda を Windows にインストールする手順」https://weblabo.oscasierra.net/python-anaconda-install-windows/ 「Anaconda を macOS にインストールする手順」https://weblabo.oscasierra.net/python-anaconda-install-macos/ いったん、anacondaがインストールされると、次の手順で、coqとcoq−jupy

9/24のマルレクでは、ソフトウェアの開発の世界の話題を取り上げます。 https://deep-spec.peatix.com/ 　 システムの大規模化・複雑化は、開発コストを増大させます。先日正式に稼働を始めたみずほ銀行のシステムMINORIは、開発に4000億円以上を投入したと言われています。 顧客に便利なサービスを事故なく提供できるのなら、必要なコストと考えてもいいと思います。それに、僕の周辺には、こうした金融機関の巨大投資を歓迎する人は、たくさんいました。IT業界にお金が流れてくるのですから。 ただ、金融の世界もITの世界も、どんどん変化していきます。開発コストの高騰は、変化への迅速な対応への足かせになる可能性があります。 もちろん、安かろう、早かろうで、バグですぐにこけるようなシステムを作っていたら、それは企業の価値を毀損することになります。ただ、大規模システムでの開発コストの低減が、今後も大きな課題になるのは確実です。 ここでは、開発コストの高騰を放置すれば、どういう事態になるかを警告した、アメリカ国防総省のDARPAのレポートを紹介したいと思います。 みずほ銀行の4000億円の開発費なんか、可愛いもんだと思うような、かつ、「ほんとかよ！」と思うような、シュールな分析がされています。DARPAすごいです。 Formal Model-Based Design & Manufacture: -- A Template for Managing Complexity in Large-Scale Cyber-Physical Systems" " https://www.innovation4.cn/library/r16328 （僕がブックマークしていた、資料のリンクが切れていて、ググり直しました。DARPAの資料を中国のサイトで読むことになってしまいました。） 直接には、F35（図１）のような軍用機の開発コストを分析しています。 図２を見てください。ここでは、大規模システムとして、三つの分野を取り上げています。CPUの開発（ピンク）、自動車の開発（グリーン）、そして軍用機の開発（パープル）です。 横軸は、部品数・ソースコードの量で計ったシステムの「複雑さ」、縦軸は、設

9/24のマルレクでは、ソフトウェアの開発の世界の話題を取り上げます。 https://deep-spec.peatix.com/ 　 ソフトウェアの開発だけでなくハードウェアの開発も、大規模化・複雑化が進んでいます。ここではCPUの開発での話題を取り上げます。 CPUの設計では、動作の徹底的なシミレーションは可能ですが、最終成果物であるCPUチップに対して、アジャイルのような開発手法はとれません。 今回のマルレクのテーマである「形式手法」は、ハードウェアの正しい動作を保証する手段として、ハードウェアの開発では重要な役割を果たしていて、すでに広く用いられていると語られてきました。 ただ、実態は、必ずしもそうでなかったようです。 RISCVチップの検証を、初めて完全に形式的手法で行うことに成功したチッパラは、次のように語っています。 http://bit.ly/2MbSdin 「ソフトウェアに関する経験しかない研究者にとっては、この業界がハードウェアに対して行なっている形式的方法というものが、いたるところで制限されたものだということに驚くことになるだろう。 そこでの形式方法というのは、典型的には、モデルのチェックと充足性の解決に基づいたもので、結局分析は明示的な状態空間の探索に還元される。 検証作業は、フルシステムの（比較的）小さなコンポーネント、例えば、プロセッサの浮動小数点ユニットに集中している。確かに、浮動小数点演算の実装アルゴリズムの完全な検証は、それ自体、英雄的な努力を必要とするのだが、これらの個々の結果は、システム全体の定理には組み込まれない。」 彼の指摘は、昨年来話題になっている、SpectreやMeltdownといった CPUアーキテクチャー設計自体の不備をつく攻撃に対する、CPUの深刻な脆弱性を考えると重要な意味を持っています。 現在のほとんど全てのCPUは「投機的実行 Speculative execution」をサポートしています。投機的実行は、条件付き分岐命令に出会うと、条件の計算が終わるのを待たずに、二つの可能な分岐をキャッシュ上で先読みして実行します。条件の計算が終わって、どちらの分岐が選択されるのか確定した時点で、一方の「当たり」のキャッシュの計算結果が採用され、一方

9/24のマルレクでは、ソフトウェアの開発の世界の話題を取り上げます。 https://deep-spec.peatix.com/ 　 システムの構築方法が変わるにつれ、開発の方法も変化します。現代のシステムは、規模の大小を問わず、またユーザ（場合によっては開発者も！）がそれを意識する否かを問わず、ネットワークをまたいでサービスを交換するのが、基本的なスタイルになっています。 こうした分散システムの開発には、そうではないモノリシックなシステムの開発とは異なる注意が必要になります。分散システム上でプログラムを正しく実行させるのは、そうでないシステム上でプログラムを正しく実行させるより、本当は、難しいのです。 先日も、AWSで大規模な障害が起きましたが、ここで取り上げたいのはそうしたことではありません。 クラウド事業者は、基本的には、分散システム設計のプロで、何が設計の肝で、トラブルにどう対応すればいいのかをよく理解していると、僕は信じています。 問題は、一般のユーザー企業も、普通のプログラマーも、そのことを意識するか否かをとわず、事実上の分散システムを作ることが、今では当たり前になっていることです。 こうした分散システムの構築の難しさによるトラブルは、枚挙にいとまがありません。 2002年4月に起きた、みずほ銀行の大規模な障害は、システム内のネットワーク、第一勧業銀行・富士銀行・日本興業銀行間を結ぶネットワークをコントロールする「リレーコンピュータ」のバグが原因でした。 写真は、2015年7月8日のシステム障害で、創設以来223年間、途絶えたことのなかった取引の中止に追い込まれたニューヨーク証券取引所の前でボーッとする人。 単純な例ですが、分散システムでのプログラミングの難しさを示した図があります。 https://github.com/…/d…/blob/master/verdi/slides/verdi-2.pdf  から。 分散システム上のノードは、故障で死んでるかもしれないし（ノード S2）、メッセージの通信がタイムアウトを起こしてメッセージが伝わっていないかもしれません（ノード S1）、またある瞬間をとれば、メッセージは送り出されているのに、まだ受け手のノードには届いていないかもしれません。 分

今回は、大規模開発の問題の事例の一回目として、航空機でのソフト開発を取り上げようと思います。 2018年10月29日、インドネシアでライオン・エアのボーイング737MAX が離陸直後に墜落、乗客乗員189名全員が死亡しました。 2019年3月10日には、エチオピアで、エチオピア航空の同じボーイング737MAX 8が、やはり離陸直後に墜落。乗客乗員157名全員が死亡しました。 墜落の原因は、MCASという自動操縦システムの不具合だと言われています。 「MCASを始動させるシグナルは、機首の角度を調べる2個のセンサー（AoA＝迎え角センサー）から出る。2個のうち1個は正常だったが、残る1個が故障して異常に高い角度を示していた。MCASは高い角度のほうに反応するので、機首が上がりすぎていると判断し、強制的に下げようとしたのである。」 http://bit.ly/2k56eCK この事故の関連では、ブルームバーグ紙が、ボーイング社は737MAXのソフトウェア開発をインドのHCLという会社に委託していて、その中には大学を出たばかりの時給9ドルの若者がいたことをすっぱ抜いて話題になりました。（ボーイング社は、今回の不具合にこの若者が関わったことを否定しています。） 現代の航空機は、「空飛ぶソフトウェア」と言われるほど、大規模なシステムなのですが、その高価なシステム開発に、時給1000円の人が使われていたのは、ちょっと驚きでしたが、僕が気になったのは、他のところです。 ブルームバーグの記事  http://bit.ly/2k56eCK  を読んでも、「仕様」はボーイング社が提供し、HCL社は「コード」を納品したことは書いてあるのですが、先の記事を見ても、不具合の原因が「仕様」の側にあったのか「コーダー」の側にあったのか判然としません。これは大事なところです。 古い、ある意味「ハード」だけで動いていた飛行機には、Fail Safe のノウハウが二重三重に生かされていたと言います。ところが、現在の旅客ジェットは、ソフトウェアの塊であるだけでなく、それ自身が「空飛ぶ大規模分散システム」になっています。 個人的には、二つのセンサーの一方（場合によったら両方）が故障したり、異なる値を返した時の処理に疑問を持っています。

「型の理論」入門 型のないラムダ計算１ https://youtu.be/WEbDbLwEog8 http://bit.ly/2MOQMr5 型のないラムダ計算２ https://youtu.be/sGhiSSNnv0Y http://bit.ly/34dma8l 型付きラムダ計算 https://youtu.be/p9dv0RH4s60 http://bit.ly/32q7GQX 論理的推論１ -- 判断と論理式 https://youtu.be/Nrv5UVeoL4o http://bit.ly/30XTf5W 論理的推論２ -- Natural Deduction https://youtu.be/J-2F2slEqu4 http://bit.ly/2NE0iNo Curry-Howard対応１ https://youtu.be/_QDaoBabMU8 http://bit.ly/2MMVJRv Curry-Howard対応２ --「型の理論」と「証明の理論」 https://youtu.be/47YanruvaLE http://bit.ly/2Uit4oe Dependent Type Theory https://youtu.be/4cH3zWEQ5ko http://bit.ly/2ZpttLu Homotopy Type Theory https://youtu.be/N92Rx4USQPY http://bit.ly/2L96rzw

As a science fiction writer who began as a fan, I do not use my fiction as a disguised way to criticize the reality of the present. I feel that the greatest appeal of science fiction is the creation of numerous imaginary worlds outside of reality. I’ve always felt that the greatest and most beautiful stories in the history of humanity were not sung by wandering bards or written by playwrights and novelists, but told by science. The stories of science are far more magnificent, grand, involved, profound, thrilling, strange, terrifying, mysterious, and even emotional, compared to the stories told by literature. 一人のファンとして始まったSF作家として、私は、現在の現実を批判するための偽装として自分の創作を利用することはない。SFの最大の魅力は、現実の外に無数の空想世界を作り出すことにあると私は感じている。私は、人類の歴史において、最大の最も美しい物語は、吟遊詩人によって歌われたものでも、戯曲家や小説家によって書かれたものでもなく、科学によって語られたものだと、いつも感じてきた。科学の物語は、はるかに壮麗で、偉大で、感動的で、深遠で、スリリングで、奇妙で、人をおののかせ、神秘的である。それは、文学によって語られる物語たちと比較しても、より感情に訴えるものでさえある。