Open 2020.01.23
ソフトウェア・エンジニアリングの新しい潮流 -- Deep Specificationの世界 #1

ソフトウェア・エンジニアリングの新しい潮流 -- Deep Specificationの世界(後半)

  • このエントリ
ーをはてなブックマークに追加
1122
2469
タグ :

■ 動画紹介

今回のマルレクでは、"Deep Specification" というソフトウェア・エンジニアリングの新しい潮流を紹介します。この流れは、ハードとソフトの開発に、コンピュータの数学的証明能力を利用して、プログラムの正しさをチェックしようというものです。

ほとんどの開発者にとっては、「機械がチェックする数学的証明」なぞは、アカデミーの世界の好奇心の対象ぐらいにしか思っていないかもしれません。プログラムの開発に「形式的手法」を導入しようという動きは、新しいものではありません。HoareのHoare Logicをはじめとして、1960年代末にはすでに生まれていました。その当時のシステムと比較して、現在のシステムは、はるかに大規模で複雑なものです。現在の大規模で複雑なシステムについても、「形式的手法」は有効なのでしょうか?

MITのアダム・チッパラ(Adam Chlpala)は、むしろ逆だといいます。

「現在利用されているコードは、ほとんど信頼性のチェックを受けていない。ただ、今後10年以内に、全てのコードが「上から下まで」(ハードウェア設計、ファームウェア、CPU、機械語、コンパイラー、開発言語、アプリケーション、仕様)、コンピュータによる信頼性チェックを受けるようになるだろう。」

「四色問題」をコンピュータを使って解いたアッペルは、"Deep Specification" を次のように説明しています。

「我々は、他の多くのプロジェクトでも使われている小規模な検証済みコンポーネントから、大規模な検証済みシステムが常に構築されている世界を期待している。そのために、全産業規模でのソフトウェアとハードウェア・コンポーネントの正式仕様の重要な基礎を明らかにしようとする」

彼らが展望している世界では、現在、開発者の日常の一部になっている「テスト」「デバッグ」「コードレビュー」は、姿を大きく変え、プログラムの開発スタイルは、大きく変わるといいます。

今回のマルレクでは、ソフトウェア・エンジニアリングの世界の未来を考えます。

■ コンテンツ一覧

視聴条件:コンテンツ一覧の動画はご購入することで全て視聴できます。


■講師・スピーカー紹介

丸山 不二夫
東京大学教育学部卒業。一橋大学大学院社会学研究科博士課程修了。稚内北星学園大学学長、早稲田大学大学院情報生産システム研究科客員教授等を歴任。オープンソースのコミュニティ活動に積極的に参加。日本Javaユーザー会名誉会長。日本Androidの会名誉会長。クラウド研究会代表。 近年では、日本のIT業界がグローバルな技術イノベーションの一翼を担うことを目標に、連続講演会「マルレク」を主宰し、クラウドコンピューティングや人工知能などの技術について講演を行っている。

丸山事務所(マルレク):  http://www.digital-life365.com/
日本Androidの会:   https://www.android-group.jp/
過去の講演資料:    https://goo.gl/XM5YsT

2016 年9月更新

  • このエントリ
ーをはてなブックマークに追加

関連動画