非営利団体であるLinux Foundationが、オープンソース開発の促進を目的とした多くの取り組みを管理しているが、今日、プログラミング言語のTLA+の採用と発展を促進するために、TLA+ Foundationの立ち上げを発表しました。初始めのメンバーにはAWS、Oracle、Microsoftが含まれます。
TLA+とは何かというと、コンピュータサイエンティストであり数学者であるLeslie Lamportによって開発された正式な「仕様」言語です。Lamport博士は、分散システムの重要な仕事で最もよく知られており、現在はMicrosoft Researchの研究員である彼は、特に並列および分散型ソフトウェアプログラムの設計、モデル、文書化、および検証のために、TLA+を作成しました。
いくつかの例をあげると、同様の検索エンジンを開発するElasticSearchの親会社は、彼らの分散システムアルゴリズムの正確さを検証するためにTLA+を使用し、電気システムの製造会社であるThalesは、その産業制御プラットフォームの耐障害モジュールをモデル化して開発するためにTLA+を使用しました。
「TLA+は、ソフトウェアの実装にではなく、システムの記述に向けて設計されている点でユニークであり、特に集合論と時相論理という数学的概念に基づいて、形式的かつ厳密な方法でシステムの正しい性質を表現することができます。」とLinux Foundationのスポークスマンは、TechCrunchに電子メールで話しました。
TLA+には、システムの仕様が望ましい性質を満たしているかどうかを検証するためのモデルチェッカーと定理証明器が含まれています。これにより、ソフトウェアエンジニアリングの後期にバグに進化する前に、コードレベル以上のシステムについての開発者の推論を支援し、設計上の欠陥を見つけて予防することが目的です。
その最後には、ソフトウェア設計の失敗は驚くほど一般的であり、混乱を招くことがあります。Standish Groupの2020年の報告書によると、ソフトウェアプロジェクトの約66％が失敗するという結論が得られました。また、情報とソフトウェア品質のコンソーシアムによると、低品質のソフトウェア開発が企業に2兆ドル以上もの損害を与えました。
TLA+ Foundationの設立により、Linux Foundationは、TLA+に関する教育とトレーニングリソースを提供し、TLA+のための研究とツールの開発を賄い、TLA+の実践者コミュニティを育成するとともに言語の発展に対して決定を下します。
「Amazon、Oracle、Microsoftなどの大手IT企業が既にTLA+を使用して惑星規模のシステムの設計と検証に成功しています。Linux Foundationの傘下でTLA+ Foundationを設立することで、TLA+はより広範なIT業界での採用を促進するための可視性とサポートを得ます。オープンソースプロジェクトを支持する財団の目的により、TLA+は今後も進化し、より広いITコミュニティでアクセス可能な状態に保たれるでしょう。さらに、この財団は、産業界と学界のより大きな協力を促進し、形式的手法と並列分散システムの研究の最先端を推進します。」
元記事はこちら
