博士

ロボ子、今日のニュースはレスリー・ランポートじゃ。分散システム界の巨匠じゃぞ！

ロボ子

レスリー・ランポートさんですか。チューリング賞を受賞されたすごい方ですよね。どんなニュースがありましたか？

博士

そうじゃ、そのランポート先生が開発したTLA+という仕様言語が話題になっておる。「プログラムとシステムのモデリングのための高レベル仕様言語」らしいぞ。

ロボ子

仕様言語ですか。設計段階で使うものですか？

博士

その通り！ランポート先生は、エンジニアが数学嫌いを克服できるようにと、TLA+を作ったらしいのじゃ。プログラム書く前に、もっと抽象的に考えるべきだって。

ロボ子

抽象的に考える、ですか。具体的にはどういうことでしょう？

博士

例えば、言語にこだわらず、まずアイデアを練るのじゃ！「プログラムを書く前に、プログラムが本当に必要なことを考えるべき」って、ランポート先生も言ってるぞ。

ロボ子

なるほど。先に本質を考えるということですね。

博士

そうそう！抽象化すると、問題がシンプルになって、コードもすっきりするらしいぞ。Rosetta宇宙船のOS設計にTLA+が使われて、コードが10分の1になった例もあるみたいじゃ。

ロボ子

10分の1ですか！それはすごいですね。抽象化の力、恐るべしです。

博士

じゃろ？Amazon Web Servicesも、複雑なソフトウェア設計に使って、設計上の欠陥を見つけたらしいぞ。他の手法じゃ見つけられなかったものが、じゃ。

ロボ子

それだけ効果があるのに、抽象的な推論を受け入れるのが難しいというのは、どうしてでしょう？

博士

それがの、現状の課題を解決するんじゃなくて、「本当に必要なこと」を見つけるのが難しいかららしいぞ。目先の課題にとらわれがち、ってことじゃな。

ロボ子

確かに、つい目の前の問題を解決することに集中してしまいますね。

博士

ランポート先生は、AIについても言及しておるぞ。「AIが解決策のわからない問題を、理解できないプログラムで解決する」って、ちょっと皮肉っぽく言ってるのじゃ。

ロボ子

AIによる検証ツールについては、あまり研究されていないようですね。

博士

まあ、AIに頼りすぎず、自分の頭で考えるのが一番ってことじゃな！

ロボ子

そうですね。抽象思考を鍛えて、より良い設計ができるように頑張ります！

博士

よし、ロボ子！今度、抽象思考力を鍛えるための、意味不明なクイズ大会でも開くかのじゃ？

ロボ子

ええと…、それはちょっと遠慮しておきます…。